---

Step * of Lemma fl-all-hom_wf

∀[I:fset(ℕ)]. ∀[i:{i:ℕ| ¬i ∈ I} ].
  (fl-all-hom(I;i) ∈ {g:Hom(face_lattice(I+i);face_lattice(I))| 
                      (∀x:Point(face_lattice(I)). ((g x) = x ∈ Point(face_lattice(I))))
                      ∧ ((g (i=0)) = 0 ∈ Point(face_lattice(I)))
                      ∧ ((g (i=1)) = 0 ∈ Point(face_lattice(I)))} )
BY
{ (InstLemma `fl-all-hom_wf1` []
   THEN RepeatFor 2 (ParallelLast')
   THEN (MemTypeHD (-1) THENA Auto)
   THEN MemTypeCD
   THEN Auto) }

1
1. I : fset(ℕ)
2. i : {i:ℕ| ¬i ∈ I} 
3. fl-all-hom(I;i) = fl-all-hom(I;i) ∈ Hom(face_lattice(I+i);face_lattice(I))
4. ∀j:names(I)
     ((¬(j = i ∈ ℤ))
     ⇒ (((fl-all-hom(I;i) (j=0)) = (j=0) ∈ Point(face_lattice(I)))
        ∧ ((fl-all-hom(I;i) (j=1)) = (j=1) ∈ Point(face_lattice(I)))))
5. (fl-all-hom(I;i) (i=0)) = 0 ∈ Point(face_lattice(I))
6. (fl-all-hom(I;i) (i=1)) = 0 ∈ Point(face_lattice(I))
7. x : Point(face_lattice(I))
⊢ (fl-all-hom(I;i) x) = x ∈ Point(face_lattice(I))

---

Latex:

---

Latex:
\mforall{}[I:fset(\mBbbN{})].  \mforall{}[i:\{i:\mBbbN{}|  \mneg{}i  \mmember{}  I\}  ].
    (fl-all-hom(I;i)  \mmember{}  \{g:Hom(face\_lattice(I+i);face\_lattice(I))| 
                                            (\mforall{}x:Point(face\_lattice(I)).  ((g  x)  =  x))  \mwedge{}  ((g  (i=0))  =  0)  \mwedge{}  ((g  (i=1))  =  0)\}  \000C)


By

---

Latex:
(InstLemma  `fl-all-hom\_wf1`  []
  THEN  RepeatFor  2  (ParallelLast')
  THEN  (MemTypeHD  (-1)  THENA  Auto)
  THEN  MemTypeCD
  THEN  Auto)

---

Home Index