---

Step * of Lemma full-partition-point-member

∀I:Interval. (icompact(I) ⇒ (∀p:partition(I). (∀x∈full-partition(I;p).x ∈ I)))
BY
{ (Auto
   THEN Unfold `full-partition` 0
   THEN (BLemma `l_all_cons` THEN Auto)
   THEN Try ((BLemma `l_all_append` THEN Auto))
   THEN Try ((BLemma `partition-point-member` THEN Complete (Auto)))
   THEN Try ((BLemma `l_all_single` THEN Auto))
   THEN BLemma `icompact-endpoints`
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}I:Interval.  (icompact(I)  {}\mRightarrow{}  (\mforall{}p:partition(I).  (\mforall{}x\mmember{}full-partition(I;p).x  \mmember{}  I)))


By

---

Latex:
(Auto
  THEN  Unfold  `full-partition`  0
  THEN  (BLemma  `l\_all\_cons`  THEN  Auto)
  THEN  Try  ((BLemma  `l\_all\_append`  THEN  Auto))
  THEN  Try  ((BLemma  `partition-point-member`  THEN  Complete  (Auto)))
  THEN  Try  ((BLemma  `l\_all\_single`  THEN  Auto))
  THEN  BLemma  `icompact-endpoints`
  THEN  Auto)

---

Home Index