mem_range_aleph_iff

Mathlib.SetTheory.Cardinal.Aleph

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

English

For any cardinal c, c ∈ range aleph iff ℵ₀ ≤ c.

Русский

Для любого кардинала c верно: c принадлежит диапазону aleph тогда и только тогда, когда ℵ₀ ≤ c.

LaTeX

$$$$ c \in \operatorname{range}(\aleph) \iff \aleph_{0} \le c. $$$$

Lean4

theorem mem_range_aleph_iff {c : Cardinal} : c ∈ range aleph ↔ ℵ₀ ≤ c := by rw [range_aleph, mem_Ici]

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

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

Разделы

Аффилиация

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