---

Step * of Lemma implies-is-partition-choice

∀I:Interval
  (icompact(I)
  ⇒ (∀p:partition(I). ∀x:partition-choice(full-partition(I;p)).  is-partition-choice(full-partition(I;p);x)))
BY
{ (Auto THEN D 0 THEN Auto THEN Unfold `partition-choice` -2 THEN GenConclTerm ⌜x i⌝⋅ THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  D  0  THEN  Auto  THEN  Unfold  `partition-choice`  -2  THEN  GenConclTerm  \mkleeneopen{}x  i\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index