mk_le_aleph0_iff

Mathlib.SetTheory.Cardinal.Basic

URI: https://scilib.ai/kg/mathlib#Cardinal.mk_le_aleph0_iff

English

For any type α, the cardinality of α is ≤ aleph0 if and only if α is countable.

Русский

Для любого типа α кардинал α ≤ aleph0 тогда и только тогда α счетінобелен.

LaTeX

$$$ \#\alpha \le \aleph_0 \iff \text{Countable } \alpha $$$

Lean4

theorem mk_le_aleph0_iff : #α ≤ ℵ₀ ↔ Countable α := by
  rw [countable_iff_nonempty_embedding, aleph0, ← lift_uzero #α, lift_mk_le']

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

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

Разделы

Аффилиация

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