---

Step * of Lemma cat-isomorphic_inversion

No Annotations
∀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@i'
2. a : cat-ob(C)@i
3. b : cat-ob(C)@i
4. f : cat-arrow(C) a b@i
5. g : cat-arrow(C) b a@i
6. fg=1
7. gf=1
⊢ cat-isomorphic(C;b;a)

---

Latex:

---

Latex:
No  Annotations
\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