k is just a notation for {0..k
}| NOTE: | k is just a notation for {0..k} |
| Who Cites int seg? | |
| int_seg |
Def {i..j} == {k: | i  k < j } |
Thm*  m,n:. {m..n}  Type | |
| int_upper |
Def {i...} == {j:| ij } |
| Thm* n:. {n...} Type | |
| wellfounded |
Def WellFnd{i}(A;x,y.R(x;y))
== P:(A  Prop). (j:A. (k:A. R(k;j)   P(k)) P(j)) {n:A. P(n)} |
| Thm* A:Type{i}, r:(AAProp{i}). WellFnd{i}(A;x,y.r(x,y)) Prop{i'} | |
| lelt |
Def i j < k == ij & j < k |
| le |
Def AB ==  B < A |
| Thm* i,j:. ij Prop | |
| not |
Def A == A False |
| Thm* A:Prop. (A) Prop |
About:
 |  |  |  |  |  |
 |  |  |  |  |
 |