Definitions graph 1 2 Sections Graphs Doc

Some definitions of interest.
increasing Def increasing(f;k) == i:(k-1). f(i) < f(i+1)
Thm* k:, f:(k). increasing(f;k) 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
length Def ||as|| == Case of as; nil 0 ; a.as' ||as'||+1 (recursive)
Thm* A:Type, l:A List. ||l||
Thm* ||nil||
map Def map(f;as) == Case of as; nil nil ; a.as' [(f(a)) / map(f;as')] (recursive)
Thm* A,B:Type, f:(AB), l:A List. map(f;l) B List
Thm* A,B:Type, f:(AB), l:A List. map(f;l) B List
nat_plus Def == {i:| 0 < i }
Thm* Type
select Def l[i] == hd(nth_tl(i;l))
Thm* A:Type, l:A List, n:. 0n n < ||l|| l[n] A

About:
listconsnillist_ind
intnatural_numberaddsubtractless_thansetapplyfunction
recursive_def_noticeuniversememberpropimpliesall
!abstraction

Definitions graph 1 2 Sections Graphs Doc