---

Step * of Lemma cat-isomorphic_inversion

∀C:SmallCategory. ∀a,b:cat-ob(C).  (cat-isomorphic(C;a;b) ⇒ cat-isomorphic(C;b;a))
BY
{ (Auto THEN RepeatFor 3 (D -1)) }

1
1. C : SmallCategory
2. a : cat-ob(C)
3. b : cat-ob(C)
4. f : cat-arrow(C) a b
5. g : cat-arrow(C) b a
6. fg=1
7. gf=1
⊢ cat-isomorphic(C;b;a)

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  RepeatFor  3  (D  -1))

---

Home Index