---

Step * 1 of Lemma partition-choice-member


1. I : Interval@i
2. icompact(I)@i
3. p : partition(I)@i
4. x : i:ℕ||full-partition(I;p)|| - 1 ⟶ {x:ℝ| x ∈ [full-partition(I;p)[i], full-partition(I;p)[i + 1]]} @i
5. i : ℕ||full-partition(I;p)|| - 1@i
6. v : {x:ℝ| x ∈ [full-partition(I;p)[i], full-partition(I;p)[i + 1]]} @i
7. (x i) = v ∈ {x:ℝ| x ∈ [full-partition(I;p)[i], full-partition(I;p)[i + 1]]} @i
⊢ v ∈ I
BY
{ (D (-2)
   THEN Unhide⋅
   THEN Auto
   THEN RepUR ``i-member rccint`` -4
   THEN InstLemma `i-member-between` [⌜I⌝;⌜full-partition(I;p)[i]⌝;⌜full-partition(I;p)[i + 1]⌝;⌜v⌝]⋅
   THEN Auto
   THEN InstLemma `full-partition-point-member` [⌜I⌝;⌜p⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:

1.  I  :  Interval@i
2.  icompact(I)@i
3.  p  :  partition(I)@i
4.  x  :  i:\mBbbN{}||full-partition(I;p)||  -  1  {}\mrightarrow{}  \{x:\mBbbR{}| 
                                                                                    x  \mmember{}  [full-partition(I;p)[i],  full-partition(I;p)[i
                                                                                            +  1]]\}  @i
5.  i  :  \mBbbN{}||full-partition(I;p)||  -  1@i
6.  v  :  \{x:\mBbbR{}|  x  \mmember{}  [full-partition(I;p)[i],  full-partition(I;p)[i  +  1]]\}  @i
7.  (x  i)  =  v@i
\mvdash{}  v  \mmember{}  I


By

---

Latex:
(D  (-2)
  THEN  Unhide\mcdot{}
  THEN  Auto
  THEN  RepUR  ``i-member  rccint``  -4
  THEN  InstLemma  `i-member-between`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}full-partition(I;p)[i]\mkleeneclose{};\mkleeneopen{}full-partition(I;p)[i  +  1]\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  InstLemma  `full-partition-point-member`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index