toOrdinal_min

Mathlib.SetTheory.Ordinal.NaturalOps

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

English

toOrdinal preserves binary minimum: toOrdinal(min a b) = min (toOrdinal a) (toOrdinal b).

Русский

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

LaTeX

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

Lean4

@[simp]
theorem toOrdinal_min (a b : NatOrdinal) : toOrdinal (min a b) = min (toOrdinal a) (toOrdinal b) :=
  rfl

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

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

Разделы

Аффилиация

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