---

Step * of Lemma fl-all-hom_wf1

∀[I:fset(ℕ)]. ∀[i:ℕ].
  (fl-all-hom(I;i) ∈ {g:Hom(face_lattice(I+i);face_lattice(I))| 
                      (∀j:names(I)
                         ((¬(j = i ∈ ℤ))
                         ⇒ (((g (j=0)) = (j=0) ∈ Point(face_lattice(I)))
                            ∧ ((g (j=1)) = (j=1) ∈ Point(face_lattice(I))))))
                      ∧ ((g (i=0)) = 0 ∈ Point(face_lattice(I)))
                      ∧ ((g (i=1)) = 0 ∈ Point(face_lattice(I)))} )
BY
{ (Auto THEN Unfold `fl-all-hom` 0 THEN DoSubsume) }

1
1. I : fset(ℕ)
2. i : ℕ
⊢ fl-lift(names(I+i);NamesDeq;face_lattice(I);face_lattice-deq();λx.if (x =z i) then 0 else (x=0) fi ;λx.if (x =z i)
                                                                                                         then 0
                                                                                                         else (x=1)
                                                                                                         fi )
  ∈ {g:Hom(face-lattice(names(I+i);NamesDeq);face_lattice(I))| 
     ∀x:names(I+i)
       (((g (x=0)) = ((λx.if (x =z i) then 0 else (x=0) fi ) x) ∈ Point(face_lattice(I)))
       ∧ ((g (x=1)) = ((λx.if (x =z i) then 0 else (x=1) fi ) x) ∈ Point(face_lattice(I))))} 

2
1. I : fset(ℕ)
2. i : ℕ
3. fl-lift(names(I+i);NamesDeq;face_lattice(I);face_lattice-deq();λx.if (x =z i) then 0 else (x=0) fi ;λx.if (x =z i)
                                                                                                          then 0
                                                                                                          else (x=1)
                                                                                                          fi )
= fl-lift(names(I+i);NamesDeq;face_lattice(I);face_lattice-deq();λx.if (x =z i) then 0 else (x=0) fi ;λx.if (x =z i)
                                                                                                         then 0
                                                                                                         else (x=1)
                                                                                                         fi )
∈ {g:Hom(face-lattice(names(I+i);NamesDeq);face_lattice(I))| 
   ∀x:names(I+i)
     (((g (x=0)) = ((λx.if (x =z i) then 0 else (x=0) fi ) x) ∈ Point(face_lattice(I)))
     ∧ ((g (x=1)) = ((λx.if (x =z i) then 0 else (x=1) fi ) x) ∈ Point(face_lattice(I))))} 
⊢ {g:Hom(face-lattice(names(I+i);NamesDeq);face_lattice(I))| 
   ∀x:names(I+i)
     (((g (x=0)) = ((λx.if (x =z i) then 0 else (x=0) fi ) x) ∈ Point(face_lattice(I)))
     ∧ ((g (x=1)) = ((λx.if (x =z i) then 0 else (x=1) fi ) x) ∈ Point(face_lattice(I))))} 
    ⊆r {g:Hom(face_lattice(I+i);face_lattice(I))| 
        (∀j:names(I)
           ((¬(j = i ∈ ℤ))
           ⇒ (((g (j=0)) = (j=0) ∈ Point(face_lattice(I))) ∧ ((g (j=1)) = (j=1) ∈ Point(face_lattice(I))))))
        ∧ ((g (i=0)) = 0 ∈ Point(face_lattice(I)))
        ∧ ((g (i=1)) = 0 ∈ Point(face_lattice(I)))} 

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  Unfold  `fl-all-hom`  0  THEN  DoSubsume)

---

Home Index