---

Step * of Lemma poset_functor_extend_same

∀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))).
∀x:cat-ob(poset-cat(I)).
  ∀[y:cat-ob(poset-cat(I))]
    poset_functor_extend(C;I;L;E;x;y) = (cat-id(C) (L x)) ∈ (cat-arrow(C) (L x) (L x)) 
    supposing x = y ∈ cat-ob(poset-cat(I))
BY
{ 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{}x:cat-ob(poset-cat(I)).
    \mforall{}[y:cat-ob(poset-cat(I))].  poset\_functor\_extend(C;I;L;E;x;y)  =  (cat-id(C)  (L  x))  supposing  x  =  y


By

---

Latex:
Auto

---

Home Index