countable

Mathlib.Data.Countable.Basic

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

English

If β is countable and f : α ↪ β, then α is countable.

Русский

Если β счётен и имеется вложение f : α ↪ β, то α счётен.

LaTeX

$$$$ \text{Countable}(\alpha) \text{ given } f : \alpha \hookrightarrow \beta \text{ and } \text{Countable}(\beta). $$$$

Lean4

protected theorem countable [Countable β] (f : α ↪ β) : Countable α :=
  f.injective.countable

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

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

Разделы

Аффилиация

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