uncountable — Mathlib

English

If β is uncountable and f: α → β is surjective, then α is uncountable.

Русский

Если β неисчисляемо и f: α → β сюръективна, тогда α неисчисляемо.

LaTeX

$$$\forall \alpha\beta\, [\operatorname{Uncountable}(\beta)]\{f:\alpha\to\beta\},\ \operatorname{Surjective}(f) \rightarrow \operatorname{Uncountable}(\alpha)$$$

Lean4

protected theorem uncountable [Uncountable β] {f : α → β} (hf : Surjective f) : Uncountable α :=
  (injective_surjInv hf).uncountable

Похожие утверждения