Step
*
of Lemma
groupoid_inv
No Annotations
∀[G:Groupoid]
∀x,y:cat-ob(cat(G)). ∀f:cat-arrow(cat(G)) x y.
(((cat-comp(cat(G)) x y x f groupoid-inv(G;x;y;f)) = (cat-id(cat(G)) x) ∈ (cat-arrow(cat(G)) x x))
∧ ((cat-comp(cat(G)) y x y groupoid-inv(G;x;y;f) f) = (cat-id(cat(G)) y) ∈ (cat-arrow(cat(G)) y y)))
BY
{ (Auto THEN D 1 THEN D 2 THEN All (RepUR ``groupoid-cat groupoid-inv``) THEN Auto) }
Latex:
Latex:
No Annotations
\mforall{}[G:Groupoid]
\mforall{}x,y:cat-ob(cat(G)). \mforall{}f:cat-arrow(cat(G)) x y.
(((cat-comp(cat(G)) x y x f groupoid-inv(G;x;y;f)) = (cat-id(cat(G)) x))
\mwedge{} ((cat-comp(cat(G)) y x y groupoid-inv(G;x;y;f) f) = (cat-id(cat(G)) y)))
By
Latex:
(Auto THEN D 1 THEN D 2 THEN All (RepUR ``groupoid-cat groupoid-inv``) THEN Auto)
Home
Index