Step
*
of Lemma
dM-to-FL-is-hom
∀[I:fset(ℕ)]. (λz.dM-to-FL(I;z) ∈ Hom(free-DeMorgan-lattice(names(I);NamesDeq);face_lattice(I)))
BY
{ Auto }
1
1. I : fset(ℕ)
⊢ λz.dM-to-FL(I;z) ∈ Hom(free-DeMorgan-lattice(names(I);NamesDeq);face_lattice(I))
Latex:
Latex:
\mforall{}[I:fset(\mBbbN{})]. (\mlambda{}z.dM-to-FL(I;z) \mmember{} Hom(free-DeMorgan-lattice(names(I);NamesDeq);face\_lattice(I)))
By
Latex:
Auto
Home
Index