Nuprl Definition : equiv-equipollent
A ~ B mod (a1,a2.E[a1; a2]) == ∃f:A ⟶ B. (Surj(A;B;f) ∧ (∀a1,a2:A. ((f a1) = (f a2) ∈ B ⇐⇒ ↓E[a1; a2])))
Definitions occuring in Statement :
surject: Surj(A;B;f),
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
iff: P ⇐⇒ Q,
squash: ↓T,
and: P ∧ Q,
apply: f a,
function: x:A ⟶ B[x],
equal: s = t ∈ T
Definitions occuring in definition :
exists: ∃x:A. B[x],
function: x:A ⟶ B[x],
and: P ∧ Q,
surject: Surj(A;B;f),
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
equal: s = t ∈ T,
apply: f a,
squash: ↓T
FDL editor aliases :
equiv-equipollent
Latex:
A \msim{} B mod (a1,a2.E[a1; a2]) ==
\mexists{}f:A {}\mrightarrow{} B. (Surj(A;B;f) \mwedge{} (\mforall{}a1,a2:A. ((f a1) = (f a2) \mLeftarrow{}{}\mRightarrow{} \mdownarrow{}E[a1; a2])))
Date html generated:
2018_05_21-PM-00_52_55
Last ObjectModification:
2018_01_11-PM-05_06_30
Theory : equipollence!!cardinality!
Home
Index