le_aleph0_iff_set_countable

Mathlib.SetTheory.Cardinal.Basic

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

English

For a set s, #s ≤ aleph0 if and only if s.Countable.

Русский

Для множества s верно: #s ≤ aleph0 тогда и только тогда sCountable.

LaTeX

$$$ #s \le \aleph_0 \iff s.Countable $$$

Lean4

theorem le_aleph0_iff_set_countable {s : Set α} : #s ≤ ℵ₀ ↔ s.Countable :=
  mk_le_aleph0_iff

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

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

Разделы

Аффилиация

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