---

Step * 2 of Lemma fl-all-hom_wf1


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)))} 
BY
{ ((Thin (-1) THEN Reduce 0) THEN (D 0 THENA Auto)) }

1
.....subterm..... T:t
1:n
1. I : fset(ℕ)
2. i : ℕ
3. x : {g:Hom(face-lattice(names(I+i);NamesDeq);face_lattice(I))| 
        ∀x:names(I+i)
          (((g (x=0)) = if (x =z i) then 0 else (x=0) fi  ∈ Point(face_lattice(I)))
          ∧ ((g (x=1)) = if (x =z i) then 0 else (x=1) fi  ∈ Point(face_lattice(I))))} 
⊢ x ∈ {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:

1.  I  :  fset(\mBbbN{})
2.  i  :  \mBbbN{}
3.  fl-lift(names(I+i);NamesDeq;face\_lattice(I);face\_lattice-deq();\mlambda{}x.if  (x  =\msubz{}  i)
                                                                                                                                          then  0
                                                                                                                                          else  (x=0)
                                                                                                                                          fi  ;\mlambda{}x.if  (x  =\msubz{}  i)
                                                                                                                                                        then  0
                                                                                                                                                        else  (x=1)
                                                                                                                                                        fi  )
=  fl-lift(names(I+i);NamesDeq;face\_lattice(I);face\_lattice-deq();
                    \mlambda{}x.if  (x  =\msubz{}  i)  then  0  else  (x=0)  fi  ;\mlambda{}x.if  (x  =\msubz{}  i)  then  0  else  (x=1)  fi  )
\mvdash{}  \{g:Hom(face-lattice(names(I+i);NamesDeq);face\_lattice(I))| 
      \mforall{}x:names(I+i)
          (((g  (x=0))  =  ((\mlambda{}x.if  (x  =\msubz{}  i)  then  0  else  (x=0)  fi  )  x))
          \mwedge{}  ((g  (x=1))  =  ((\mlambda{}x.if  (x  =\msubz{}  i)  then  0  else  (x=1)  fi  )  x)))\} 
        \msubseteq{}r  \{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:
((Thin  (-1)  THEN  Reduce  0)  THEN  (D  0  THENA  Auto))

---

Home Index