---

Step * of Lemma cat-isomorphic_transitivity

∀C:SmallCategory. ∀a,b,c:cat-ob(C).  (cat-isomorphic(C;a;b) ⇒ cat-isomorphic(C;b;c) ⇒ cat-isomorphic(C;a;c))
BY
{ (Auto THEN D -2 THEN D -1 THEN D 0 With ⌜cat-comp(C) a b c f f1⌝  THEN EAuto 1) }

---

Latex:

---

Latex:
\mforall{}C:SmallCategory.  \mforall{}a,b,c:cat-ob(C).
    (cat-isomorphic(C;a;b)  {}\mRightarrow{}  cat-isomorphic(C;b;c)  {}\mRightarrow{}  cat-isomorphic(C;a;c))


By

---

Latex:
(Auto  THEN  D  -2  THEN  D  -1  THEN  D  0  With  \mkleeneopen{}cat-comp(C)  a  b  c  f  f1\mkleeneclose{}    THEN  EAuto  1)

---

Home Index