---

Step * 1 of Lemma fl-morph-id


1. I : fset(ℕ)
2. x : names(I)
⊢ (x=0) = dM-to-FL(I;¬(<x>)) ∈ Point(face_lattice(I))
BY
{ (RWW "neg-dM_inc dM-to-FL-inc dM-to-FL-opp" 0 THEN Try ((Folds ``fl1 fl0`` 0 THEN EqCD)) THEN Auto) }

---

Latex:

---

Latex:

1.  I  :  fset(\mBbbN{})
2.  x  :  names(I)
\mvdash{}  (x=0)  =  dM-to-FL(I;\mneg{}(<x>))


By

---

Latex:
(RWW  "neg-dM\_inc  dM-to-FL-inc  dM-to-FL-opp"  0  THEN  Try  ((Folds  ``fl1  fl0``  0  THEN  EqCD))  THEN  Auto)

---

Home Index