cast_max

Mathlib.Algebra.Order.Ring.Cast

URI: https://scilib.ai/kg/mathlib#Int.cast_max

English

The cast of the maximum equals the maximum of the casts: ↑max(a,b) cast = max(a cast, b cast).

Русский

Приведение максимума равняется максимуму приведения двух аргументов.

LaTeX

$$↑\max(a,b)^{\mathsf{cast}} = \max(a^{\mathsf{cast}}, b^{\mathsf{cast}})$$

Lean4

@[simp, norm_cast]
theorem cast_max : (↑(max a b) : R) = max (a : R) (b : R) :=
  Monotone.map_max cast_mono

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

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

Разделы

Аффилиация

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