| Some definitions of interest. |
|
int_lower | Def {...i} == {j: | j i } |
| | Thm* i: . {...i} Type |
|
int_seg | Def {i..j } == {k: | i k < j } |
| | Thm* m,n: . {m..n } Type |
|
int_upper | Def {i...} == {j: | i j } |
| | Thm* n: . {n...} Type |
|
is_ident | Def is_ident(A; f; u) == x:A. f(u,x) = x & f(x,u) = x |
| | Thm* f:(A![](FONT/dash.png) A![](FONT/dash.png) A), u:A. is_ident(A; f; u) Prop |
|
iter_via_intseg | Def Iter(f;u) i:{a..b }. e(i)
Def == if a< b f((Iter(f;u) i:{a..b-1 }. e(i)),e(b-1)) else u fi
Def (recursive) |
| | Thm* f:(A![](FONT/dash.png) A![](FONT/dash.png) A), u:A, a,b: , e:({a..b }![](FONT/dash.png) A). (Iter(f;u) i:{a..b }. e(i)) A |