card_le_iff

Mathlib.SetTheory.Ordinal.Basic

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

English

Let o be an ordinal and c a cardinal. Then o.card ≤ c if and only if o < (succ c).ord.

Русский

Пусть o — ординал, а c — кардинал. Тогда |o| ≤ c тогда же, когда o < ord(succ c).

LaTeX

$$$ |o| \le c \iff o < \operatorname{ord}(\operatorname{succ} c) $$$

Lean4

theorem card_le_iff {o : Ordinal} {c : Cardinal} : o.card ≤ c ↔ o < (succ c).ord := by rw [lt_ord, lt_succ_iff]

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

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

Разделы

Аффилиация

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