---

Step * 1 of Lemma fl-morph-face-lattice1


1. J : fset(ℕ)
2. I : fset(ℕ)
3. f : J ⟶ I
4. x : names(I)
5. v : {g:Hom(face-lattice(names(I);NamesDeq);face_lattice(J))| 
        ∀x:names(I)
          (((g (x=0)) = ((λj.dM-to-FL(J;¬(f j))) x) ∈ Point(face_lattice(J)))
          ∧ ((g (x=1)) = ((λj.dM-to-FL(J;f j)) x) ∈ Point(face_lattice(J))))} 
6. fl-lift(names(I);NamesDeq;face_lattice(J);face_lattice-deq();λj.dM-to-FL(J;¬(f j));λj.dM-to-FL(J;f j))
= v
∈ {g:Hom(face-lattice(names(I);NamesDeq);face_lattice(J))| 
   ∀x:names(I)
     (((g (x=0)) = ((λj.dM-to-FL(J;¬(f j))) x) ∈ Point(face_lattice(J)))
     ∧ ((g (x=1)) = ((λj.dM-to-FL(J;f j)) x) ∈ Point(face_lattice(J))))} 
⊢ (v (x=1)) = dM-to-FL(J;f x) ∈ Point(face_lattice(J))
BY
{ ((Reduce (-2) THEN D -2) THEN Auto) }

---

Latex:

---

Latex:

1.  J  :  fset(\mBbbN{})
2.  I  :  fset(\mBbbN{})
3.  f  :  J  {}\mrightarrow{}  I
4.  x  :  names(I)
5.  v  :  \{g:Hom(face-lattice(names(I);NamesDeq);face\_lattice(J))| 
                \mforall{}x:names(I)
                    (((g  (x=0))  =  ((\mlambda{}j.dM-to-FL(J;\mneg{}(f  j)))  x))  \mwedge{}  ((g  (x=1))  =  ((\mlambda{}j.dM-to-FL(J;f  j))  x)))\} 
6.  fl-lift(names(I);NamesDeq;face\_lattice(J);face\_lattice-deq();\mlambda{}j.dM-to-FL(J;\mneg{}(f  j));
                      \mlambda{}j.dM-to-FL(J;f  j))
=  v
\mvdash{}  (v  (x=1))  =  dM-to-FL(J;f  x)


By

---

Latex:
((Reduce  (-2)  THEN  D  -2)  THEN  Auto)

---

Home Index