toNimber_max

Mathlib.SetTheory.Nimber.Basic

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

English

Nimber respects taking maximum: the nimber of max(a,b) is max of nimbers.

Русский

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

LaTeX

$$$\\\\forall a\\\\ b: \\\\mathrm{Ordinal}, \\\\ast(\\\\max a b) = \\\\max( \\\\ast a, \\\\ast b).$$$

Lean4

@[simp]
theorem toNimber_max (a b : Ordinal) : ∗(max a b) = max (∗a) (∗b) :=
  rfl

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

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

Разделы

Аффилиация

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