coe_max

Mathlib.Data.NNReal.Defs

URI: https://scilib.ai/kg/mathlib#NNReal.coe_max

English

Let x, y be nonnegative numbers. Then ((max x y) : ℝ) = max (x : ℝ) (y : ℝ).

Русский

Пусть x, y ∈ ℝ≥0. Тогда ((max x y) : ℝ) = max(x, y) в ℝ.

LaTeX

$$$$ ((\\max x y) : \\mathbb{R}) = \\max(x, y). $$$$

Lean4

@[simp, norm_cast]
theorem coe_max (x y : ℝ≥0) : ((max x y : ℝ≥0) : ℝ) = max (x : ℝ) (y : ℝ) :=
  NNReal.coe_mono.map_max

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

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

Разделы

Аффилиация

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