---

Step * of Lemma partition-refines_wf

∀I:Interval. ∀P,Q:partition(I).  (P refines Q ∈ ℙ) supposing icompact(I)
BY
{ (Unfold `partition-refines` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}I:Interval.  \mforall{}P,Q:partition(I).    (P  refines  Q  \mmember{}  \mBbbP{})  supposing  icompact(I)


By

---

Latex:
(Unfold  `partition-refines`  0  THEN  Auto)

---

Home Index