ord_card_le

Mathlib.SetTheory.Ordinal.Basic

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

English

For every ordinal o, ord(#α).ord ≤ o if and only if α's card ≤ o.card.

Русский

Для каждого ординала o: ord(#α).ord ≤ o тогда и только тогда, когда card(α) ≤ o.card.

LaTeX

$$$\operatorname{ord}(\#\alpha).\ord \le o \iff \#\alpha \le o.card$$$

Lean4

theorem ord_card_le (o : Ordinal) : o.card.ord ≤ o :=
  gc_ord_card.l_u_le _

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

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

Разделы

Аффилиация

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