---

Step * 2 of Lemma dM-to-FL-eq-1


1. I : fset(ℕ)
2. x : Point(dM(I))
3. x = 1 ∈ Point(dM(I))
⊢ dM-to-FL(I;x) = 1 ∈ Point(face_lattice(I))
BY
{ ((HypSubst'(-1) 0 THEN Auto) THEN InstLemma `dM-to-FL-properties` [⌜I⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  I  :  fset(\mBbbN{})
2.  x  :  Point(dM(I))
3.  x  =  1
\mvdash{}  dM-to-FL(I;x)  =  1


By

---

Latex:
((HypSubst'(-1)  0  THEN  Auto)  THEN  InstLemma  `dM-to-FL-properties`  [\mkleeneopen{}I\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index