| Some definitions of interest. |
|
compose | Def (f o g)(x) == f(g(x)) |
| | Thm* A,B,C:Type, f:(B![](FONT/dash.png) C), g:(A![](FONT/dash.png) B). f o g A![](FONT/dash.png) C |
|
flip | Def (i, j)(x) == if x= i j ; x= j i else x fi |
| | Thm* k: , i,j: k. (i, j) k![](FONT/dash.png) ![](FONT/then_med.png) k |
|
int_seg | Def {i..j } == {k: | i k < j } |
| | Thm* m,n: . {m..n } Type |