---

Step * of Lemma partition-mesh-nil

∀[I:Top]. (partition-mesh(I;[]) ~ |I|)
BY
{ (Intros THEN RepUR ``partition-mesh full-partition frs-mesh rmaximum`` 0 THEN Fold `i-length` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[I:Top].  (partition-mesh(I;[])  \msim{}  |I|)


By

---

Latex:
(Intros
  THEN  RepUR  ``partition-mesh  full-partition  frs-mesh  rmaximum``  0
  THEN  Fold  `i-length`  0
  THEN  Auto)

---

Home Index