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 30996
 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 ↦ (𝑏 ∈ 𝒫 ℕ, 𝑚 ∈ ℤ ↦ {𝑐 ∈ (𝑏𝑚 (0..^𝑠)) ∣ Σ𝑎 ∈ (0..^𝑠)(𝑐𝑎) = 𝑚}))
Distinct variable group:   𝑎,𝑏,𝑐,𝑚,𝑠

Detailed syntax breakdown of Definition df-repr
StepHypRef Expression
1 crepr 30995 . 2 class repr
2 vs . . 3 setvar 𝑠
3 cn0 11484 . . 3 class 0
4 vb . . . 4 setvar 𝑏
5 vm . . . 4 setvar 𝑚
6 cn 11212 . . . . 5 class
76cpw 4302 . . . 4 class 𝒫 ℕ
8 cz 11569 . . . 4 class
9 cc0 10128 . . . . . . . 8 class 0
102cv 1631 . . . . . . . 8 class 𝑠
11 cfzo 12659 . . . . . . . 8 class ..^
129, 10, 11co 6813 . . . . . . 7 class (0..^𝑠)
13 va . . . . . . . . 9 setvar 𝑎
1413cv 1631 . . . . . . . 8 class 𝑎
15 vc . . . . . . . . 9 setvar 𝑐
1615cv 1631 . . . . . . . 8 class 𝑐
1714, 16cfv 6049 . . . . . . 7 class (𝑐𝑎)
1812, 17, 13csu 14615 . . . . . 6 class Σ𝑎 ∈ (0..^𝑠)(𝑐𝑎)
195cv 1631 . . . . . 6 class 𝑚
2018, 19wceq 1632 . . . . 5 wff Σ𝑎 ∈ (0..^𝑠)(𝑐𝑎) = 𝑚
214cv 1631 . . . . . 6 class 𝑏
22 cmap 8023 . . . . . 6 class 𝑚
2321, 12, 22co 6813 . . . . 5 class (𝑏𝑚 (0..^𝑠))
2420, 15, 23crab 3054 . . . 4 class {𝑐 ∈ (𝑏𝑚 (0..^𝑠)) ∣ Σ𝑎 ∈ (0..^𝑠)(𝑐𝑎) = 𝑚}
254, 5, 7, 8, 24cmpt2 6815 . . 3 class (𝑏 ∈ 𝒫 ℕ, 𝑚 ∈ ℤ ↦ {𝑐 ∈ (𝑏𝑚 (0..^𝑠)) ∣ Σ𝑎 ∈ (0..^𝑠)(𝑐𝑎) = 𝑚})
262, 3, 25cmpt 4881 . 2 class (𝑠 ∈ ℕ0 ↦ (𝑏 ∈ 𝒫 ℕ, 𝑚 ∈ ℤ ↦ {𝑐 ∈ (𝑏𝑚 (0..^𝑠)) ∣ Σ𝑎 ∈ (0..^𝑠)(𝑐𝑎) = 𝑚}))
271, 26wceq 1632 1 wff repr = (𝑠 ∈ ℕ0 ↦ (𝑏 ∈ 𝒫 ℕ, 𝑚 ∈ ℤ ↦ {𝑐 ∈ (𝑏𝑚 (0..^𝑠)) ∣ Σ𝑎 ∈ (0..^𝑠)(𝑐𝑎) = 𝑚}))
 Colors of variables: wff setvar class This definition is referenced by:  reprval  30997
 Copyright terms: Public domain W3C validator