---

Step * 1 of Lemma partition-choice-indep-funtype

.....subterm..... T:t
1:n
1. I : Interval
2. icompact(I)
3. p : partition(I)
4. ||full-partition(I;p)|| = (||p|| + 2) ∈ ℤ
5. x : partition-choice(full-partition(I;p))
⊢ x ∈ ℕ||p|| + 1 ⟶ {x:ℝ| x ∈ I} 
BY
{ ((FunExt THENA Auto)
   THEN DoSubsume
   THEN Auto
   THEN (D 0 THENA Auto)
   THEN D -1
   THEN MemTypeCD
   THEN Auto
   THEN (InstLemma `full-partition-point-member` [⌜I⌝;⌜p⌝]⋅ THENA Auto)
   THEN DupHyp (-1)
   THEN (D -1 With ⌜x1⌝  THENA Auto)
   THEN MoveToConcl (-1)
   THEN (D -1 With ⌜x1 + 1⌝  THENA Auto)
   THEN RepeatFor 2 (MoveToConcl (-1))
   THEN GenConclTerms Auto [⌜full-partition(I;p)[x1]⌝;⌜full-partition(I;p)[x1 + 1]⌝]⋅
   THEN All Thin
   THEN Auto
   THEN (InstLemma `i-member-between` [⌜I⌝;⌜v⌝;⌜v1⌝]⋅ THENA Auto)
   THEN BHyp -1 
   THEN Auto) }

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
1.  I  :  Interval
2.  icompact(I)
3.  p  :  partition(I)
4.  ||full-partition(I;p)||  =  (||p||  +  2)
5.  x  :  partition-choice(full-partition(I;p))
\mvdash{}  x  \mmember{}  \mBbbN{}||p||  +  1  {}\mrightarrow{}  \{x:\mBbbR{}|  x  \mmember{}  I\} 


By

---

Latex:
((FunExt  THENA  Auto)
  THEN  DoSubsume
  THEN  Auto
  THEN  (D  0  THENA  Auto)
  THEN  D  -1
  THEN  MemTypeCD
  THEN  Auto
  THEN  (InstLemma  `full-partition-point-member`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  DupHyp  (-1)
  THEN  (D  -1  With  \mkleeneopen{}x1\mkleeneclose{}    THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  (D  -1  With  \mkleeneopen{}x1  +  1\mkleeneclose{}    THENA  Auto)
  THEN  RepeatFor  2  (MoveToConcl  (-1))
  THEN  GenConclTerms  Auto  [\mkleeneopen{}full-partition(I;p)[x1]\mkleeneclose{};\mkleeneopen{}full-partition(I;p)[x1  +  1]\mkleeneclose{}]\mcdot{}
  THEN  All  Thin
  THEN  Auto
  THEN  (InstLemma  `i-member-between`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{};\mkleeneopen{}v1\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  BHyp  -1 
  THEN  Auto)

---

Home Index