countable

Mathlib.Data.Countable.Defs

URI: https://scilib.ai/kg/mathlib#Function.Surjective.countable

English

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

Русский

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

LaTeX

$$$ \operatorname{Countable}(\alpha) \land \operatorname{Surjective}(f) \Rightarrow \operatorname{Countable}(\beta) $$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru