---

Step * of Lemma fl-morph-face-lattice1

∀[J,I:fset(ℕ)]. ∀[f:J ⟶ I]. ∀[x:names(I)].  (((x=1))<f> = dM-to-FL(J;f x) ∈ Point(face_lattice(J)))
BY
{ (Auto
   THEN RepUR ``fl-morph`` 0
   THEN (GenConclTerm ⌜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))⌝⋅
         THENA Auto
         )) }

1
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))

---

Latex:

---

Latex:
\mforall{}[J,I:fset(\mBbbN{})].  \mforall{}[f:J  {}\mrightarrow{}  I].  \mforall{}[x:names(I)].    (((x=1))<f>  =  dM-to-FL(J;f  x))


By

---

Latex:
(Auto
  THEN  RepUR  ``fl-morph``  0
  THEN  (GenConclTerm  \mkleeneopen{}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))\mkleeneclose{}\mcdot{}
              THENA  Auto
              ))

---

Home Index