Nuprl - Some Definitions

	Some definitions of interest.

list-connect	`Def L-G- > x == (yL.y-G- > x)`

connect	`Def x-the_graph- > *y == p:Vertices(the_graph) List. path(the_graph;p) & p[0] = x & last(p) = y`

	`Thm* For any graph x,y:V. x-the_graph- > *y Prop`

gr_v	`Def Vertices(t) == 1of(t)`

	`Thm* t:Graph. Vertices(t) Type`

graph	`Def Graph == v:Typee:Type(evv)Top`

	`Thm* Graph Type{i'}`

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

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

l_exists	`Def (xL.P(x)) == x:T. (x L) & P(x)`

	`Thm* T:Type, L:T List, P:(TProp). (xL.P(x)) Prop`

About: