---

Step * of Lemma dM-to-FL-inc

∀[I:fset(ℕ)]. ∀[x:names(I)].  (dM-to-FL(I;<x>) = (x=1) ∈ Point(face_lattice(I)))
BY
{ (Auto
   THEN Unfold `dM-to-FL` 0
   THEN RepUR ``dM_opp dM_inc dmopp dminc`` 0
   THEN ((RWO "lattice-extend-dl-inc" 0 THENM Reduce 0) THENA Auto)) }

---

Latex:

---

Latex:
\mforall{}[I:fset(\mBbbN{})].  \mforall{}[x:names(I)].    (dM-to-FL(I;<x>)  =  (x=1))


By

---

Latex:
(Auto
  THEN  Unfold  `dM-to-FL`  0
  THEN  RepUR  ``dM\_opp  dM\_inc  dmopp  dminc``  0
  THEN  ((RWO  "lattice-extend-dl-inc"  0  THENM  Reduce  0)  THENA  Auto))

---

Home Index