---

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

∀I:fset(ℕ)
  ∀[h:Hom(face_lattice(I);face_lattice(I))]
    h = (λx.x) ∈ Hom(face_lattice(I);face_lattice(I)) 
    supposing ∀x:names(I). (((h (x=0)) = (x=0) ∈ Point(face_lattice(I))) ∧ ((h (x=1)) = (x=1) ∈ Point(face_lattice(I))))
BY
{ (Auto
   THEN All (Unfolds ``face_lattice fl0 fl1``)
   THEN (InstLemma `face-lattice-hom-unique` [names(I);NamesDeq;⌜face-lattice(names(I);NamesDeq)⌝;⌜face_lattice-deq()⌝;
         ⌜λx.(x=0)⌝;⌜λx.(x=1)⌝]⋅
         THENA (Auto THEN Try ((Fold `face_lattice` 0 THEN Auto)))
         )
   THEN BHyp -1 
   THEN Auto) }

1
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))

---

Latex:

---

Latex:
\mforall{}I:fset(\mBbbN{})
    \mforall{}[h:Hom(face\_lattice(I);face\_lattice(I))]
        h  =  (\mlambda{}x.x)  supposing  \mforall{}x:names(I).  (((h  (x=0))  =  (x=0))  \mwedge{}  ((h  (x=1))  =  (x=1)))


By

---

Latex:
(Auto
  THEN  All  (Unfolds  ``face\_lattice  fl0  fl1``)
  THEN  (InstLemma  `face-lattice-hom-unique`  [names(I);NamesDeq;\mkleeneopen{}face-lattice(names(I);NamesDeq)\mkleeneclose{};
              \mkleeneopen{}face\_lattice-deq()\mkleeneclose{};\mkleeneopen{}\mlambda{}x.(x=0)\mkleeneclose{};\mkleeneopen{}\mlambda{}x.(x=1)\mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  Try  ((Fold  `face\_lattice`  0  THEN  Auto)))
              )
  THEN  BHyp  -1 
  THEN  Auto)

---

Home Index