toNatOrdinal_max

Mathlib.SetTheory.Ordinal.NaturalOps

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

English

NatOrdinal preserves binary maximum: the nat image of max equals the max of nat images.

Русский

Пусть max — это максимум по ординалам; тогда toNatOrdinal(max(a,b)) = max(toNatOrdinal(a), toNatOrdinal(b)).

LaTeX

$$$toNatOrdinal(\max(a,b)) = \max( toNatOrdinal(a), toNatOrdinal(b) )$$$

Lean4

@[simp]
theorem toNatOrdinal_max (a b : Ordinal) : toNatOrdinal (max a b) = max (toNatOrdinal a) (toNatOrdinal b) :=
  rfl

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

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

Разделы

Аффилиация

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