Definitions
graph
1
1
Sections
Graphs
Doc
Some definitions of interest.
ge
Def
i
j == j
i
Thm*
i,j:
. (i
j)
Prop
gt
Def
i > j == j < i
Thm*
i,j:
. (i > j)
Prop
int_lower
Def
{...i} == {j:
| j
i }
Thm*
i:
. {...i}
Type
int_nzero
Def
== {i:
| i
0 }
Thm*
Type
nat
Def
== {i:
| 0
i }
Thm*
Type
le
Def
A
B ==
B < A
Thm*
i,j:
. (i
j)
Prop
nat_plus
Def
== {i:
| 0 < i }
Thm*
Type
not
Def
A == A
False
Thm*
A:Prop. (
A)
Prop
About:
Definitions
graph
1
1
Sections
Graphs
Doc