Def  InvFuns(A;B;f;g) == (x:A. g(f(x)) = x) & (y:B. f(g(y)) = y)

is mentioned by

Thm*  f:(a bij a). InvFuns(a;a;f;y.least x:. f(x)=y)	[nsub_bij_least_preimage_inverse]
Thm*  InvFuns(A;A;f;g)  (i:. InvFuns(A;A;f{i};g{i}))	[compose_iter_inverses]
Thm*  InvFuns(;{xy:()| xy = <0,0>   };next_nat_pair;prev_nat_pair)	[next_nat_pair_vs_prev_nat_pair]
Thm*  InvFuns(A+B;i:2if i=0 A else B fi;union_to_sigma;sigma_to_union)	[union_sigma_inverses]
Thm*  f:(AB). Bij(A; B; f)  (g:(BA). InvFuns(A;B;f;g))	[bij_imp_exists_inv2]
Thm*  f:(AB). Bij(A; B; f)  (g:(BA). InvFuns(A;B;f;g))	[bij_imp_exists_inv_version2]
Thm*  f:(AB), g:(BA). InvFuns(A;B;f;g)  Bij(A; B; f)	[fun_with_inv_is_bij_version2]
Thm*  InvFuns(A;B;f;g)  Bij(B; A; g)	[fun_with_inv2_is_bij_rev]
Thm*  InvFuns(A;B;f;g)  Bij(A; B; f)	[fun_with_inv2_is_bij]
Thm*  InvFuns(A;B;f;g)  InvFuns(A;B;f;h)  g = h	[inv_funs_2_unique]
Thm*  InvFuns(A;B;f;g)  Surj(B; A; g)	[fun_with_inv2_is_surj_rev]
Thm*  InvFuns(A;B;f;g)  Inj(A; B; f) & Inj(B; A; g)	[invfuns_are_inj]
Thm*  InvFuns(A;B;f;g)  Inj(B; A; g)	[fun_with_inv2_is_inj_rev]
Thm*  InvFuns(A;B;f;g)  Surj(A; B; f) & Surj(B; A; g)	[invfuns_are_surj]
Thm*  InvFuns(A;B;f;g)  InvFuns(B;A;g;f)	[inv_funs_2_sym]
Thm*  R:(ABProp).  Thm*  (1-1-Corr x:A,y:B. R(x;y)) Thm*   Thm*  (f:(AB), g:(BA). Thm*  (InvFuns(A;B;f;g) & (x:A, y:B. R(x;y)  y = f(x) & x = g(y)))	[one_one_corr_rel_vs_invfuns]
Thm*  InvFuns(A; B; f; g)  InvFuns(A;B;f;g)	[inv_funs_iff_inv_funs_2]
Thm*  f:(AB), g:(BA). SqStable(InvFuns(A;B;f;g))	[sq_stable__inv_funs_2]
Thm*  InvFuns(A;B;f;g)  Surj(A; B; f)	[fun_with_inv2_is_surj]
Thm*  InvFuns(A;B;f;g)  Inj(A; B; f)	[fun_with_inv2_is_inj]
Thm*  InvFuns(A;A;Id;Id)	[inv_funs_2_identity]
Def  AB == {fg:((AB)(BA))| fg/f,g. InvFuns(A;B;f;g) }	[inv_pair]
Def  f is 1-1 corr == g:(BA). InvFuns(A;B;f;g)	[is_one_one_corr]
Def  (x:A. B(x)) ~ (x':A'. B'(x')) Def  == f:(AA'), g:(A'A), F:(x:AB(x)B'(f(x))), G:(x:AB'(f(x))B(x)). Def  == InvFuns(A;A';f;g) & (u:A. InvFuns(B(u);B'(f(u));F(u);G(u)))	[one_one_corr_fams]
Def  A ~ B == f:(AB), g:(BA). InvFuns(A;B;f;g)	[one_one_corr_2]

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