| Some definitions of interest. |
|
biject | Def Bij(A; B; f) == Inj(A; B; f) & Surj(A; B; f) |
| | Thm* A,B:Type, f:(A![](FONT/dash.png) B). Bij(A; B; f) Prop |
|
one_one_corr_fams | Def (x:A. B(x)) ~ (x':A'. B'(x'))
Def == f:(A![](FONT/dash.png) A'), g:(A'![](FONT/dash.png) A), F:(x:A![](FONT/dash.png) B(x)![](FONT/dash.png) B'(f(x))), G:(x:A![](FONT/dash.png) B'(f(x))![](FONT/dash.png) B(x)).
Def == InvFuns(A;A';f;g) & ( u:A. InvFuns(B(u);B'(f(u));F(u);G(u))) |
| | Thm* A:Type, A':Type, B:(A![](FONT/dash.png) Type), B':(A'![](FONT/dash.png) Type).
Thm* ((x:A. B(x)) ~ (x':A'. B'(x'))) Prop |