toNatOrdinal_min

Mathlib.SetTheory.Ordinal.NaturalOps

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

English

NatOrdinal preserves binary minimum: the nat image of min equals the min of nat images.

Русский

Пусть min — это минимум; тогда toNatOrdinal(min(a,b)) = min(toNatOrdinal(a), toNatOrdinal(b)).

LaTeX

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

Lean4

@[simp]
theorem toNatOrdinal_min (a b : Ordinal) : toNatOrdinal (min a b) = min (toNatOrdinal a) (toNatOrdinal b) :=
  rfl

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

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

Разделы

Аффилиация

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