| Some definitions of interest. |
|
biject | Def Bij(A; B; f) == Inj(A; B; f) & Surj(A; B; f) |
| | Thm* A,B:Type, f:(AB). Bij(A; B; f) Prop |
|
equiv_rel | Def EquivRel x,y:T. E(x;y)
Def == Refl(T;x,y.E(x;y)) & (Sym x,y:T. E(x;y)) & (Trans x,y:T. E(x;y)) |
| | Thm* T:Type, E:(TTProp). (EquivRel x,y:T. E(x;y)) Prop |
|
iff | Def P Q == (P Q) & (P Q) |
| | Thm* A,B:Prop. (A B) Prop |
|
inject | Def Inj(A; B; f) == a1,a2:A. f(a1) = f(a2) B a1 = a2 |
| | Thm* A,B:Type, f:(AB). Inj(A; B; f) Prop |
|
int_seg | Def {i..j} == {k:| i k < j } |
| | Thm* m,n:. {m..n} Type |
|
nat | Def == {i:| 0i } |
| | Thm* Type |
|
le | Def AB == B<A |
| | Thm* i,j:. (ij) Prop |
|
one_one_corr_2 | Def A ~ B == f:(AB), g:(BA). InvFuns(A;B;f;g) |
| | Thm* A,B:Type. (A ~ B) Prop |
|
surject | Def Surj(A; B; f) == b:B. a:A. f(a) = b |
| | Thm* A,B:Type, f:(AB). Surj(A; B; f) Prop |