not_surjective_countable_uncountable

English

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

Русский

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

LaTeX

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

Lean4

theorem not_surjective_countable_uncountable [Countable α] [Uncountable β] (f : α → β) : ¬Surjective f := fun hf ↦
  not_countable hf.countable

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