---

Step * of Lemma member-i-type

∀[I:Interval]. ∀[r:ℝ]. ∀[p:r ∈ I].  (<i-witness(I;r;p), r> ∈ i-type(I))
BY
{ (Unfold `i-type` 0 THEN (Auto THEN MemTypeCD THEN Auto) THEN BLemma `i-witness-property` THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[I:Interval].  \mforall{}[r:\mBbbR{}].  \mforall{}[p:r  \mmember{}  I].    (<i-witness(I;r;p),  r>  \mmember{}  i-type(I))


By

---

Latex:
(Unfold  `i-type`  0  THEN  (Auto  THEN  MemTypeCD  THEN  Auto)  THEN  BLemma  `i-witness-property`  THEN  Auto)

---

Home Index