Nuprl - Some Definitions

	Who Cites col?

col	`Def Collection(T) == TProp`

	`Thm* T:Type{i'}. col{i:l}(T) Type{i'}`

col_all	`Def (xc.P(x)) == x:T. x c P(x)`

	`Thm* T:Type, c:Collection(T), P:(TProp). (xc.P(x)) Prop`

col_equal	`Def c1 = c2 == x:T. x c1 x c2`

	`Thm* T:Type, c1,c2:Collection(T). c1 = c2 Prop`

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

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

col_member	`Def x c == c(x)`

	`Thm* T:Type, x:T, c:Collection(T). x c Prop`

rev_implies	`Def P Q == Q P`

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

About: