---

Step * 1 of Lemma fl-all-hom_wf1


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))))} 
BY
{ (Auto
   THEN Try ((FLemma `not-added-name` [-2] THEN Auto))
   THEN (BoolCase ⌜(x =z i)⌝⋅ THENA Auto)
   THEN Try ((FLemma `not-added-name` [-1] THEN Auto))
   THEN Auto) }

---

Latex:

---

Latex:

1.  I  :  fset(\mBbbN{})
2.  i  :  \mBbbN{}
\mvdash{}  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  )
    \mmember{}  \{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)))\} 


By

---

Latex:
(Auto
  THEN  Try  ((FLemma  `not-added-name`  [-2]  THEN  Auto))
  THEN  (BoolCase  \mkleeneopen{}(x  =\msubz{}  i)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Try  ((FLemma  `not-added-name`  [-1]  THEN  Auto))
  THEN  Auto)

---

Home Index