---

Step * of Lemma poset_functor_extend-flip

∀C:SmallCategory. ∀I:Cname List. ∀L:name-morph(I;[]) ⟶ cat-ob(C). ∀E:i:nameset(I)
                                                                      ⟶ c:{c:name-morph(I;[])| (c i) = 0 ∈ ℕ2} 
                                                                      ⟶ (cat-arrow(C) (L c) (L flip(c;i))).
∀i:nameset(I). ∀c:cat-ob(poset-cat(I)).
  poset_functor_extend(C;I;L;E;c;flip(c;i)) = (E i c) ∈ (cat-arrow(C) (L c) (L flip(c;i))) supposing (c i) = 0 ∈ ℕ2
BY
{ (InstLemma `poset_functor_extend-extends` []
   THEN RepeatFor 4 (ParallelLast')
   THEN Auto
   THEN D -4
   THEN RepUR ``functor-arrow`` -4
   THEN BHyp -4 
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}C:SmallCategory.  \mforall{}I:Cname  List.  \mforall{}L:name-morph(I;[])  {}\mrightarrow{}  cat-ob(C).  \mforall{}E:i:nameset(I)
                                                                                                                                            {}\mrightarrow{}  c:\{c:name-morph(I;[])| 
                                                                                                                                                        (c  i)  =  0\} 
                                                                                                                                            {}\mrightarrow{}  (cat-arrow(C)  (L  c) 
                                                                                                                                                    (L  flip(c;i))).
\mforall{}i:nameset(I).  \mforall{}c:cat-ob(poset-cat(I)).
    poset\_functor\_extend(C;I;L;E;c;flip(c;i))  =  (E  i  c)  supposing  (c  i)  =  0


By

---

Latex:
(InstLemma  `poset\_functor\_extend-extends`  []
  THEN  RepeatFor  4  (ParallelLast')
  THEN  Auto
  THEN  D  -4
  THEN  RepUR  ``functor-arrow``  -4
  THEN  BHyp  -4 
  THEN  Auto)

---

Home Index