toENat_ne_top

Mathlib.SetTheory.Cardinal.ENat

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

English

toENat a is not the top iff a < aleph0.

Русский

toENat a не равен верхнему элементу тогда и только тогда, когда a < ℵ₀.

LaTeX

$$$toENat a \\neq \\top \\iff a < \\aleph_0$$$

Lean4

theorem toENat_ne_top {a : Cardinal} : toENat a ≠ ⊤ ↔ a < ℵ₀ := by simp

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

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

Разделы

Аффилиация

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