Def P  Q == PQ

is mentioned by

Thm* f:(AB), g:(BA). InvFuns(A; B; f; g)  Bij(A; B; f)	[fun_with_inv_is_bij]
Thm* f:(AB). Bij(A; B; f)  (g:(BA). InvFuns(A; B; f; g))	[bij_imp_exists_inv]
Thm* B:(AType), Q:(x:AB(x)Type). Thm* (x:A. y:B(x). Q(x,y))  (f:(x:AB(x)). x:A. Q(x,f(x)))	[dep_ax_choice]
Thm* Q:(ABProp). (x:A. y:B. Q(x,y))  (f:(AB). x:A. Q(x,f(x)))	[ax_choice]
Def Inj(A; B; f) == a1,a2:A. f(a1) = f(a2)  B  a1 = a2	[inject]

In prior sections: core

Try larger context: StandardLIB IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html