---

Step * 4 of Lemma face_lattice-hom-fixes-sublattice


1. I : fset(ℕ)
2. J : fset(ℕ)
3. J ⊆ I
4. f : Hom(face_lattice(J);face_lattice(I))
5. ∀i:names(J). (((f (i=0)) = (i=0) ∈ Point(face_lattice(I))) ∧ ((f (i=1)) = (i=1) ∈ Point(face_lattice(I))))
6. x : Point(face_lattice(J))
7. (f x) = x ∈ Point(face_lattice(I))
8. i : names(J)
⊢ (f (i=0) ∧ x) = (i=0) ∧ x ∈ Point(face_lattice(I))
BY
{ (RepeatFor 2 (DVar `f') THEN RWO "5.1<" 0 THEN Auto) }

1
1. I : fset(ℕ)
2. J : fset(ℕ)
3. J ⊆ I
4. f : Point(face_lattice(J)) ⟶ Point(face_lattice(I))
5. ∀[a,b:Point(face_lattice(J))].
     ((f a ∧ f b = (f a ∧ b) ∈ Point(face_lattice(I))) ∧ (f a ∨ f b = (f a ∨ b) ∈ Point(face_lattice(I))))
6. (f 0) = 0 ∈ Point(face_lattice(I))
7. (f 1) = 1 ∈ Point(face_lattice(I))
8. ∀i:names(J). (((f (i=0)) = (i=0) ∈ Point(face_lattice(I))) ∧ ((f (i=1)) = (i=1) ∈ Point(face_lattice(I))))
9. x : Point(face_lattice(J))
10. (f x) = x ∈ Point(face_lattice(I))
11. i : names(J)
⊢ f (i=0) ∧ f x = (i=0) ∧ x ∈ Point(face_lattice(I))

---

Latex:

---

Latex:

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


By

---

Latex:
(RepeatFor  2  (DVar  `f')  THEN  RWO  "5.1<"  0  THEN  Auto)

---

Home Index