Nuprl Definition : finite'
finite'(T) == ∀f:T ⟶ T. (Inj(T;T;f) ⇒ Surj(T;T;f))
Definitions occuring in Statement :
surject: Surj(A;B;f),
inject: Inj(A;B;f),
all: ∀x:A. B[x],
implies: P ⇒ Q,
function: x:A ⟶ B[x]
Definitions occuring in definition :
surject: Surj(A;B;f),
inject: Inj(A;B;f),
implies: P ⇒ Q,
function: x:A ⟶ B[x],
all: ∀x:A. B[x]
FDL editor aliases :
finite'
Latex:
finite'(T) == \mforall{}f:T {}\mrightarrow{} T. (Inj(T;T;f) {}\mRightarrow{} Surj(T;T;f))
Date html generated:
2016_10_21-AM-10_59_36
Last ObjectModification:
2016_08_06-PM-02_26_58
Theory : equipollence!!cardinality!
Home
Index