---

Step * 2 of Lemma face_lattice-hom-fixes-sublattice2


1. I : fset(ℕ)
2. J : fset(ℕ)
3. J ⊆ I
4. f : Hom(face_lattice(I);face_lattice(J))
5. ∀i:names(J). (((f (i=0)) = (i=0) ∈ Point(face_lattice(J))) ∧ ((f (i=1)) = (i=1) ∈ Point(face_lattice(J))))
⊢ (f 1) = 1 ∈ Point(face_lattice(J))
BY
{ (DVar `f' THEN Auto) }

---

Latex:

---

Latex:

1.  I  :  fset(\mBbbN{})
2.  J  :  fset(\mBbbN{})
3.  J  \msubseteq{}  I
4.  f  :  Hom(face\_lattice(I);face\_lattice(J))
5.  \mforall{}i:names(J).  (((f  (i=0))  =  (i=0))  \mwedge{}  ((f  (i=1))  =  (i=1)))
\mvdash{}  (f  1)  =  1


By

---

Latex:
(DVar  `f'  THEN  Auto)

---

Home Index