toOrdinal_max — Mathlib

English

Ordinal representation preserves the maximum: toOrdinal(max(a,b)) = max(toOrdinal(a), toOrdinal(b)).

Русский

Представление через ординалы сохраняет максимум: toOrdinal(max(a,b)) = max(toOrdinal(a), toOrdinal(b)).

LaTeX

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

Lean4

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

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