Nuprl Definition : one_one_corr
1-1-Corresp(A;B) == ∃f:A ⟶ B. ∃g:B ⟶ A. InvFuns(A;B;f;g)
Definitions occuring in Statement :
inv_funs: InvFuns(A;B;f;g),
exists: ∃x:A. B[x],
function: x:A ⟶ B[x]
Definitions occuring in definition :
exists: ∃x:A. B[x],
function: x:A ⟶ B[x],
inv_funs: InvFuns(A;B;f;g)
FDL editor aliases :
one_one_corr
Latex:
1-1-Corresp(A;B) == \mexists{}f:A {}\mrightarrow{} B. \mexists{}g:B {}\mrightarrow{} A. InvFuns(A;B;f;g)
Date html generated:
2016_05_13-PM-04_04_43
Last ObjectModification:
2015_09_22-PM-05_45_49
Theory : fun_1
Home
Index