---

Step * 1 of Lemma fl-morph-comp


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)))
BY
{ (Reduce (-1)
   THEN (InstHyp [⌜<g> o <f>⌝] (-1)⋅ THENM (Fold `fl-morph` (-1) THEN Auto))
   THEN ((BLemma `compose-bounded-lattice-hom` THEN Auto)
   ORELSE (Reduce 0 THEN RepeatFor 2 (Thin (-1)) THEN (D 0 THENA Auto))
   )) }

1
1. I : fset(ℕ)
2. J : fset(ℕ)
3. K : fset(ℕ)
4. f : J ⟶ I
5. g : K ⟶ J
6. x : names(I)
⊢ ((((x=0))<f>)<g> = dM-to-FL(K;¬(f ⋅ g x)) ∈ Point(face_lattice(K)))
∧ ((((x=1))<f>)<g> = dM-to-FL(K;f ⋅ g x) ∈ Point(face_lattice(K)))

---

Latex:

---

Latex:

1.  I  :  fset(\mBbbN{})
2.  J  :  fset(\mBbbN{})
3.  K  :  fset(\mBbbN{})
4.  f  :  J  {}\mrightarrow{}  I
5.  g  :  K  {}\mrightarrow{}  J
6.  \mforall{}[f0,f1:names(I)  {}\mrightarrow{}  Point(face\_lattice(K))].
          \mforall{}g:Hom(face\_lattice(I);face\_lattice(K))
              fl-lift(names(I);NamesDeq;face\_lattice(K);face\_lattice-deq();f0;f1)  =  g 
              supposing  \mforall{}x:names(I).  (((g  (x=0))  =  (f0  x))  \mwedge{}  ((g  (x=1))  =  (f1  x))) 
          supposing  \mforall{}x:names(I).  (f0  x  \mwedge{}  f1  x  =  0)
7.  \mforall{}g@0:Hom(face\_lattice(I);face\_lattice(K))
          fl-lift(names(I);NamesDeq;face\_lattice(K);face\_lattice-deq();\mlambda{}j.dM-to-FL(K;\mneg{}(f  \mcdot{}  g  j));
                          \mlambda{}j.dM-to-FL(K;f  \mcdot{}  g  j))
          =  g@0 
          supposing  \mforall{}x:names(I)
                                  (((g@0  (x=0))  =  ((\mlambda{}j.dM-to-FL(K;\mneg{}(f  \mcdot{}  g  j)))  x))
                                  \mwedge{}  ((g@0  (x=1))  =  ((\mlambda{}j.dM-to-FL(K;f  \mcdot{}  g  j))  x)))
\mvdash{}  <f  \mcdot{}  g>  =  (<g>  o  <f>)


By

---

Latex:
(Reduce  (-1)
  THEN  (InstHyp  [\mkleeneopen{}<g>  o  <f>\mkleeneclose{}]  (-1)\mcdot{}  THENM  (Fold  `fl-morph`  (-1)  THEN  Auto))
  THEN  ((BLemma  `compose-bounded-lattice-hom`  THEN  Auto)
  ORELSE  (Reduce  0  THEN  RepeatFor  2  (Thin  (-1))  THEN  (D  0  THENA  Auto))
  ))

---

Home Index