Nuprl - Some Definitions

card_ge	`Def \|S\| \|T\| == f:(ST). Surj(S; T; f)` `Thm* S,T:Type. \|S\| \|T\| Prop`
card_le	`Def \|S\| \|T\| == f:(ST). Inj(S; T; f)` `Thm* S,T:Type. \|S\| \|T\| Prop`
surject	`Def Surj(A; B; f) == b:B. a:A. f(a) = b` `Thm* A,B:Type, f:(AB). Surj(A; B; f) Prop`
inject	`Def Inj(A; B; f) == a1,a2:A. f(a1) = f(a2) B a1 = a2` `Thm* A,B:Type, f:(AB). Inj(A; B; f) Prop`

About: