| | Some definitions of interest. |
|
| eq_int | Def i= j == if i=j true ; false fi |
|
| | Thm*  i,j: . (i=j)   |
|
| eqfun_p | Def IsEqFun(T;eq) == x,y:T.  (x eq y)   x = y |
|
| | Thm* T:Type, eq:(T  T). IsEqFun(T;eq) Prop |
|
| int_seg | Def {i..j } == {k:| i  k < j } |
|
| | Thm* m,n:. {m..n} Type |
|
| least | Def least i: . p(i) == if p(0) 0 else (least i:. p(i+1))+1 fi (recursive) |
|
| | Thm* k:, p:{p:(k)|  i:k. p(i) }. (least i:. p(i)) k |
|
| | Thm* p:{p:()| i:. p(i) }. (least i:. p(i)) |
|
| nat | Def == {i:| 0i } |
|
| | Thm* Type |
|
| so_lambda2 | Def ( 1,2. b(1;2))(1,2) == b(1;2) |
|
| surjection_type | Def A onto B == {f:(AB)| Surj(A; B; f) } |
|
| | Thm* A,B:Type. A onto B Type |
