exists_injective_nat

Mathlib.Data.Countable.Defs

URI: https://scilib.ai/kg/mathlib#Countable.exists_injective_nat

English

If α is countable, there exists an injection f: α → ℕ.

Русский

Пусть α счётно; существует инъекция f: α → ℕ.

LaTeX

$$$ \operatorname{Countable}(\alpha) \Rightarrow \exists f : \alpha \to \mathbb{N}, \operatorname{Injective}(f) $$$

Lean4

theorem exists_injective_nat (α : Sort u) [Countable α] : ∃ f : α → ℕ, Injective f :=
  Countable.exists_injective_nat'

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

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

Разделы

Аффилиация

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