of_surjective_from_set — Mathlib

English

If a surjective map from α to β exists and β is infinite, then α is infinite.

Русский

Если существует сюръективное отображение α → β и β бесконечен, то α бесконечен.

LaTeX

$$$\\{f: \\alpha \\to \\beta\\},\\ Surjective(f) \\wedge Infinite(\\beta) \\Rightarrow Infinite(\\alpha)$$$

Lean4

/-- If `s : Set α` is a proper subset of `α` and `f : s → α` is surjective, then `α` is infinite. -/
theorem of_surjective_from_set {s : Set α} (hs : s ≠ Set.univ) {f : s → α} (hf : Surjective f) : Infinite α :=
  of_injective_to_set hs (injective_surjInv hf)

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