Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-repr Structured version   Visualization version   GIF version

Definition df-repr 31875
Description: The representations of a nonnegative 𝑚 as the sum of 𝑠 nonnegative integers from a set 𝑏. Cf. Definition of [Nathanson] p. 123. (Contributed by Thierry Arnoux, 1-Dec-2021.)
Assertion
Ref Expression
df-repr repr = (𝑠 ∈ ℕ0 ↦ (𝑏 ∈ 𝒫 ℕ, 𝑚 ∈ ℤ ↦ {𝑐 ∈ (𝑏m (0..^𝑠)) ∣ Σ𝑎 ∈ (0..^𝑠)(𝑐𝑎) = 𝑚}))
Distinct variable group:   𝑎,𝑏,𝑐,𝑚,𝑠

Detailed syntax breakdown of Definition df-repr
StepHypRef Expression
1 crepr 31874 . 2 class repr
2 vs . . 3 setvar 𝑠
3 cn0 11891 . . 3 class 0
4 vb . . . 4 setvar 𝑏
5 vm . . . 4 setvar 𝑚
6 cn 11632 . . . . 5 class
76cpw 4539 . . . 4 class 𝒫 ℕ
8 cz 11975 . . . 4 class
9 cc0 10531 . . . . . . . 8 class 0
102cv 1532 . . . . . . . 8 class 𝑠
11 cfzo 13027 . . . . . . . 8 class ..^
129, 10, 11co 7150 . . . . . . 7 class (0..^𝑠)
13 va . . . . . . . . 9 setvar 𝑎
1413cv 1532 . . . . . . . 8 class 𝑎
15 vc . . . . . . . . 9 setvar 𝑐
1615cv 1532 . . . . . . . 8 class 𝑐
1714, 16cfv 6350 . . . . . . 7 class (𝑐𝑎)
1812, 17, 13csu 15036 . . . . . 6 class Σ𝑎 ∈ (0..^𝑠)(𝑐𝑎)
195cv 1532 . . . . . 6 class 𝑚
2018, 19wceq 1533 . . . . 5 wff Σ𝑎 ∈ (0..^𝑠)(𝑐𝑎) = 𝑚
214cv 1532 . . . . . 6 class 𝑏
22 cmap 8400 . . . . . 6 class m
2321, 12, 22co 7150 . . . . 5 class (𝑏m (0..^𝑠))
2420, 15, 23crab 3142 . . . 4 class {𝑐 ∈ (𝑏m (0..^𝑠)) ∣ Σ𝑎 ∈ (0..^𝑠)(𝑐𝑎) = 𝑚}
254, 5, 7, 8, 24cmpo 7152 . . 3 class (𝑏 ∈ 𝒫 ℕ, 𝑚 ∈ ℤ ↦ {𝑐 ∈ (𝑏m (0..^𝑠)) ∣ Σ𝑎 ∈ (0..^𝑠)(𝑐𝑎) = 𝑚})
262, 3, 25cmpt 5139 . 2 class (𝑠 ∈ ℕ0 ↦ (𝑏 ∈ 𝒫 ℕ, 𝑚 ∈ ℤ ↦ {𝑐 ∈ (𝑏m (0..^𝑠)) ∣ Σ𝑎 ∈ (0..^𝑠)(𝑐𝑎) = 𝑚}))
271, 26wceq 1533 1 wff repr = (𝑠 ∈ ℕ0 ↦ (𝑏 ∈ 𝒫 ℕ, 𝑚 ∈ ℤ ↦ {𝑐 ∈ (𝑏m (0..^𝑠)) ∣ Σ𝑎 ∈ (0..^𝑠)(𝑐𝑎) = 𝑚}))
Colors of variables: wff setvar class
This definition is referenced by:  reprval  31876
  Copyright terms: Public domain W3C validator