| Some definitions of interest. |
|
delete_fenum_value | Def Replace value k by f(m) in f == Replace values x s.t. x=k by f(m) in f |
| | Thm* Inj({k:| P(k) }; {k:| Q(k) }; f)
Thm*
Thm* (m:{u:| P(u) }, k:{v:| Q(v) }.
Thm* ((Replace value k by f(m) in f)
Thm* ( {u:| P(u) & u = m }{v:| Q(v) & v = k }) |
| | Thm* Inj((m+1); (k+1); f) (Replace value k by f(m) in f) mk |
|
eq_int | Def i=j == if i=j true ; false fi |
| | Thm* i,j:. (i=j) |
|
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 |
|
nequal | Def a b T == a = b T |
| | Thm* A:Type, x,y:A. (x y) Prop |
|
one_one_corr_2 | Def A ~ B == f:(AB), g:(BA). InvFuns(A;B;f;g) |
| | Thm* A,B:Type. (A ~ B) Prop |
|
replace_fn_values | Def (Replace values x s.t. P(x) by y in f)(i) == if P(f(i)) y else f(i) fi |
| | Thm* A,X:Type, P:(A), y:A, f:(XA).
Thm* (Replace values x s.t. P(x) by y in f) XA |