---

Step * of Lemma dM-to-FL-unique

∀[I:fset(ℕ)]. ∀[g:Hom(free-DeMorgan-lattice(names(I);NamesDeq);face_lattice(I))].
  ∀[x:Point(dM(I))]. (dM-to-FL(I;x) = (g x) ∈ Point(face_lattice(I))) 
  supposing ∀i:names(I). (((g <i>) = (i=1) ∈ Point(face_lattice(I))) ∧ ((g <1-i>) = (i=0) ∈ Point(face_lattice(I))))
BY
{ Auto }

1
1. I : fset(ℕ)
2. g : Hom(free-DeMorgan-lattice(names(I);NamesDeq);face_lattice(I))
3. ∀i:names(I). (((g <i>) = (i=1) ∈ Point(face_lattice(I))) ∧ ((g <1-i>) = (i=0) ∈ Point(face_lattice(I))))
4. x : Point(dM(I))
⊢ dM-to-FL(I;x) = (g x) ∈ Point(face_lattice(I))

---

Latex:

---

Latex:
\mforall{}[I:fset(\mBbbN{})].  \mforall{}[g:Hom(free-DeMorgan-lattice(names(I);NamesDeq);face\_lattice(I))].
    \mforall{}[x:Point(dM(I))].  (dM-to-FL(I;x)  =  (g  x)) 
    supposing  \mforall{}i:names(I).  (((g  <i>)  =  (i=1))  \mwedge{}  ((g  ə-i>)  =  (i=0)))


By

---

Latex:
Auto

---

Home Index