toENat_eq_top

Mathlib.SetTheory.Cardinal.ENat

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

English

Let a be a cardinal. Then toENat a equals the top element if and only if a ≥ aleph0.

Русский

Пусть a — кардинал. Тогда toENat a равно верхнему элементу тогда и только тогда, когда a ≥ ℵ₀.

LaTeX

$$$toENat a = \\top \\iff \\aleph_0 \\le a$$$

Lean4

@[simp]
theorem toENat_eq_top {a : Cardinal} : toENat a = ⊤ ↔ ℵ₀ ≤ a :=
  enat_gc.u_eq_top

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

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

Разделы

Аффилиация

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