aleph0_le_card

Mathlib.SetTheory.Ordinal.Basic

URI: https://scilib.ai/kg/mathlib#Ordinal.aleph0_le_card

English

If c ≠ 0, then the type c.ord.toType has a least element (is an ordered set with bottom).

Русский

Если c ≠ 0, то тип c.ord.toType имеет наименьший элемент (существует элемент снизу).

LaTeX

$$IsBottom(c.ord.toType)$$

Lean4

@[simp]
theorem aleph0_le_card {o} : ℵ₀ ≤ card o ↔ ω ≤ o := by rw [← ord_le, ord_aleph0]

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

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

Разделы

Аффилиация

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