uncountable — Mathlib

English

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

Русский

Если α неисчисляема и функция f: α → β инъективна, то β неисчисляемо.

LaTeX

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

Lean4

protected theorem uncountable [Uncountable α] {f : α → β} (hf : Injective f) : Uncountable β :=
  ⟨fun _ ↦ not_countable hf.countable⟩

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