---

Step * 1 of Lemma face-lattice-hom-is-id


1. I : fset(ℕ)
2. h : Hom(face-lattice(names(I);NamesDeq);face-lattice(names(I);NamesDeq))
3. ∀x:names(I)
     (((h (x=0)) = (x=0) ∈ Point(face-lattice(names(I);NamesDeq)))
     ∧ ((h (x=1)) = (x=1) ∈ Point(face-lattice(names(I);NamesDeq))))
4. ∀[g,h:Hom(face-lattice(names(I);NamesDeq);face-lattice(names(I);NamesDeq))].
     g = h ∈ Hom(face-lattice(names(I);NamesDeq);face-lattice(names(I);NamesDeq)) 
     supposing (∀x:names(I). (g (x=0) ∧ g (x=1) = 0 ∈ Point(face-lattice(names(I);NamesDeq))))
     ∧ (∀x:names(I). ((g (x=0)) = (h (x=0)) ∈ Point(face-lattice(names(I);NamesDeq))))
     ∧ (∀x:names(I). ((g (x=1)) = (h (x=1)) ∈ Point(face-lattice(names(I);NamesDeq))))
5. x : names(I)
⊢ h (x=0) ∧ h (x=1) = 0 ∈ Point(face-lattice(names(I);NamesDeq))
BY
{ (RWO "3.1 3.2" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  I  :  fset(\mBbbN{})
2.  h  :  Hom(face-lattice(names(I);NamesDeq);face-lattice(names(I);NamesDeq))
3.  \mforall{}x:names(I).  (((h  (x=0))  =  (x=0))  \mwedge{}  ((h  (x=1))  =  (x=1)))
4.  \mforall{}[g,h:Hom(face-lattice(names(I);NamesDeq);face-lattice(names(I);NamesDeq))].
          g  =  h 
          supposing  (\mforall{}x:names(I).  (g  (x=0)  \mwedge{}  g  (x=1)  =  0))
          \mwedge{}  (\mforall{}x:names(I).  ((g  (x=0))  =  (h  (x=0))))
          \mwedge{}  (\mforall{}x:names(I).  ((g  (x=1))  =  (h  (x=1))))
5.  x  :  names(I)
\mvdash{}  h  (x=0)  \mwedge{}  h  (x=1)  =  0


By

---

Latex:
(RWO  "3.1  3.2"  0  THEN  Auto)

---

Home Index