Nuprl - Some Definitions

	Some definitions of interest.

divides	`Def b \| a == c:. a = bc`

	`Thm* a,b:. (a \| b) Prop`

graph-isomorphic	`Def G H == vmap:(Vertices(G)Vertices(H)), emap:(Edges(G)Edges(H)). Bij(Vertices(G); Vertices(H); vmap) & Bij(Edges(G); Edges(H); emap) & (vmap,vmap) o Incidence(G) = Incidence(H) o emap`

iff	`Def P Q == (P Q) & (P Q)`

	`Thm* A,B:Prop. (A B) Prop`

nat_plus	`Def == {i:\| 0 < i }`

	`Thm* Type`

rel-graph	`Def Graph(x,y:T. R(x;y)) == < vertices = T, edges = {p:(TT)\| R(1of(p);2of(p)) }, incidence = Id >`

About: