toOrdinal_max

Mathlib.SetTheory.Ordinal.NaturalOps

URI: https://scilib.ai/kg/mathlib#NatOrdinal.toOrdinal_max

English

toOrdinal preserves binary maximum: toOrdinal(max a b) = max (toOrdinal a) (toOrdinal b).

Русский

toOrdinal сохраняет максимум: toOrdinal(max(a,b)) = max(toOrdinal(a), toOrdinal(b)).

LaTeX

$$$\\mathrm{toOrdinal}(\\max(a,b)) = \\max(\\mathrm{toOrdinal}(a), \\mathrm{toOrdinal}(b))$$$

Lean4

@[simp]
theorem toOrdinal_max (a b : NatOrdinal) : toOrdinal (max a b) = max (toOrdinal a) (toOrdinal b) :=
  rfl

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

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

Разделы

Аффилиация

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