Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-iccp Structured version   Visualization version   GIF version

Definition df-iccp 41878
Description: Define partitions of a closed interval of extended reals. Such partitions are finite increasing sequences of extended reals. (Contributed by AV, 8-Jul-2020.)
Assertion
Ref Expression
df-iccp RePart = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ*𝑚 (0...𝑚)) ∣ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1))})
Distinct variable group:   𝑖,𝑚,𝑝

Detailed syntax breakdown of Definition df-iccp
StepHypRef Expression
1 ciccp 41877 . 2 class RePart
2 vm . . 3 setvar 𝑚
3 cn 11232 . . 3 class
4 vi . . . . . . . 8 setvar 𝑖
54cv 1631 . . . . . . 7 class 𝑖
6 vp . . . . . . . 8 setvar 𝑝
76cv 1631 . . . . . . 7 class 𝑝
85, 7cfv 6049 . . . . . 6 class (𝑝𝑖)
9 c1 10149 . . . . . . . 8 class 1
10 caddc 10151 . . . . . . . 8 class +
115, 9, 10co 6814 . . . . . . 7 class (𝑖 + 1)
1211, 7cfv 6049 . . . . . 6 class (𝑝‘(𝑖 + 1))
13 clt 10286 . . . . . 6 class <
148, 12, 13wbr 4804 . . . . 5 wff (𝑝𝑖) < (𝑝‘(𝑖 + 1))
15 cc0 10148 . . . . . 6 class 0
162cv 1631 . . . . . 6 class 𝑚
17 cfzo 12679 . . . . . 6 class ..^
1815, 16, 17co 6814 . . . . 5 class (0..^𝑚)
1914, 4, 18wral 3050 . . . 4 wff 𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1))
20 cxr 10285 . . . . 5 class *
21 cfz 12539 . . . . . 6 class ...
2215, 16, 21co 6814 . . . . 5 class (0...𝑚)
23 cmap 8025 . . . . 5 class 𝑚
2420, 22, 23co 6814 . . . 4 class (ℝ*𝑚 (0...𝑚))
2519, 6, 24crab 3054 . . 3 class {𝑝 ∈ (ℝ*𝑚 (0...𝑚)) ∣ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1))}
262, 3, 25cmpt 4881 . 2 class (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ*𝑚 (0...𝑚)) ∣ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1))})
271, 26wceq 1632 1 wff RePart = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ*𝑚 (0...𝑚)) ∣ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1))})
Colors of variables: wff setvar class
This definition is referenced by:  iccpval  41879
  Copyright terms: Public domain W3C validator