graph
1
1
Sections
Graphs
Doc
Def
InvFuns(A; B; f; g) == g o f = Id & f o g = Id
is mentioned by
Thm*
f:(A
B). Bij(A; B; f)
(
g:(B
A). Bij(B; A; g) & InvFuns(A; B; f; g))
[inverse-biject]
In prior sections:
fun
1
Try larger context:
Graphs
graph
1
1
Sections
Graphs
Doc
f:(A
B). Bij(A; B; f) 
(
g:(BA). Bij(B; A; g) & InvFuns(A; B; f; g))f:(AB). Bij(A; B; f) (g:(BA). Bij(B; A; g) & InvFuns(A; B; f; g))