Nuprl Definition : equipollent

==  ∃f:A ⟶ B. Bij(A;B;f)



Definitions occuring in Statement :  biject: Bij(A;B;f) exists: x:A. B[x] function: x:A ⟶ B[x]
Definitions occuring in definition :  exists: x:A. B[x] function: x:A ⟶ B[x] biject: Bij(A;B;f)
FDL editor aliases :  equipollent

Latex:
A  \msim{}  B  ==    \mexists{}f:A  {}\mrightarrow{}  B.  Bij(A;B;f)



Date html generated: 2016_05_14-PM-03_59_40
Last ObjectModification: 2015_09_22-PM-06_02_02

Theory : equipollence!!cardinality!


Home Index