card_eq_top_of_infinite

Mathlib.SetTheory.Cardinal.Finite

URI: https://scilib.ai/kg/mathlib#ENat.card_eq_top_of_infinite

English

If α is infinite, then the ENat cardinal of α equals the top element ⊤.

Русский

Если α бесконечен, то кардинал ENat α равен верхнему элементу ⊤.

LaTeX

$$$\operatorname{ENat}.card(\alpha) = \top$$$

Lean4

@[simp high]
theorem card_eq_top_of_infinite [Infinite α] : card α = ⊤ := by simp only [card, toENat_eq_top, aleph0_le_mk]

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

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

Разделы

Аффилиация

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