---

Step * of Lemma fl-morph-comp

∀[I,J,K:fset(ℕ)]. ∀[f:J ⟶ I]. ∀[g:K ⟶ J].
  (<f ⋅ g> = (<g> o <f>) ∈ (Point(face_lattice(I)) ⟶ Point(face_lattice(K))))
BY
{ (Auto
   THEN (InstLemma `fl-lift-unique` [names(I);⌜NamesDeq⌝;⌜face-lattice(names(K);NamesDeq)⌝;⌜face_lattice-deq()⌝]⋅
         THENA (Auto THEN Try ((Fold `face_lattice` 0 THEN Auto)))
         )
   THEN Fold `face_lattice` (-1)
   THEN (InstHyp [⌜λj.dM-to-FL(K;¬(f ⋅ g j))⌝;⌜λj.dM-to-FL(K;f ⋅ g j)⌝] (-1)⋅ THENA (Reduce 0 THEN Auto))) }

1
1. I : fset(ℕ)
2. J : fset(ℕ)
3. K : fset(ℕ)
4. f : J ⟶ I
5. g : K ⟶ J
6. ∀[f0,f1:names(I) ⟶ Point(face_lattice(K))].
     ∀g:Hom(face_lattice(I);face_lattice(K))
       fl-lift(names(I);NamesDeq;face_lattice(K);face_lattice-deq();f0;f1) = g ∈ Hom(face_lattice(I);face_lattice(K)) 
       supposing ∀x:names(I)
                   (((g (x=0)) = (f0 x) ∈ Point(face_lattice(K))) ∧ ((g (x=1)) = (f1 x) ∈ Point(face_lattice(K)))) 
     supposing ∀x:names(I). (f0 x ∧ f1 x = 0 ∈ Point(face_lattice(K)))
7. ∀g@0:Hom(face_lattice(I);face_lattice(K))
     fl-lift(names(I);NamesDeq;face_lattice(K);face_lattice-deq();λj.dM-to-FL(K;¬(f ⋅ g j));λj.dM-to-FL(K;f ⋅ g j))
     = g@0
     ∈ Hom(face_lattice(I);face_lattice(K)) 
     supposing ∀x:names(I)
                 (((g@0 (x=0)) = ((λj.dM-to-FL(K;¬(f ⋅ g j))) x) ∈ Point(face_lattice(K)))
                 ∧ ((g@0 (x=1)) = ((λj.dM-to-FL(K;f ⋅ g j)) x) ∈ Point(face_lattice(K))))
⊢ <f ⋅ g> = (<g> o <f>) ∈ (Point(face_lattice(I)) ⟶ Point(face_lattice(K)))

---

Latex:

---

Latex:
\mforall{}[I,J,K:fset(\mBbbN{})].  \mforall{}[f:J  {}\mrightarrow{}  I].  \mforall{}[g:K  {}\mrightarrow{}  J].    (<f  \mcdot{}  g>  =  (<g>  o  <f>))


By

---

Latex:
(Auto
  THEN  (InstLemma  `fl-lift-unique`  [names(I);\mkleeneopen{}NamesDeq\mkleeneclose{};\mkleeneopen{}face-lattice(names(K);NamesDeq)\mkleeneclose{};
              \mkleeneopen{}face\_lattice-deq()\mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  Try  ((Fold  `face\_lattice`  0  THEN  Auto)))
              )
  THEN  Fold  `face\_lattice`  (-1)
  THEN  (InstHyp  [\mkleeneopen{}\mlambda{}j.dM-to-FL(K;\mneg{}(f  \mcdot{}  g  j))\mkleeneclose{};\mkleeneopen{}\mlambda{}j.dM-to-FL(K;f  \mcdot{}  g  j)\mkleeneclose{}]  (-1)\mcdot{}
  THENA  (Reduce  0  THEN  Auto)
  ))

---

Home Index