---

Step * of Lemma partition-choice-indep-funtype

∀[I:Interval]
  ∀[p:partition(I)]. (partition-choice(full-partition(I;p)) ⊆r (ℕ||p|| + 1 ⟶ {x:ℝ| x ∈ I} )) supposing icompact(I)
BY
{ ((Auto THEN (Assert ||full-partition(I;p)|| = (||p|| + 2) ∈ ℤ BY (Unfold `full-partition` 0 THEN Auto')))
   THEN (D 0 THENA Auto)
   ) }

1
.....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} 

---

Latex:

---

Latex:
\mforall{}[I:Interval]
    \mforall{}[p:partition(I)].  (partition-choice(full-partition(I;p))  \msubseteq{}r  (\mBbbN{}||p||  +  1  {}\mrightarrow{}  \{x:\mBbbR{}|  x  \mmember{}  I\}  )) 
    supposing  icompact(I)


By

---

Latex:
((Auto
    THEN  (Assert  ||full-partition(I;p)||  =  (||p||  +  2)  BY
                            (Unfold  `full-partition`  0  THEN  Auto'))
    )
  THEN  (D  0  THENA  Auto)
  )

---

Home Index