toNimber_min

Mathlib.SetTheory.Nimber.Basic

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

English

Nimber respects taking minimum: the nimber of min(a,b) equals min of nimbers.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem toNimber_min (a b : Ordinal) : ∗(min a b) = min (∗a) (∗b) :=
  rfl

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

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

Разделы

Аффилиация

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