not_injective_uncountable_countable

English

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

Русский

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

LaTeX

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

Lean4

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

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