coe_max — Mathlib

English

For x,y in the nonnegative rationals, the natural cast of max(x,y) equals the maximum of the casts: ((max x y) : ℚ) = max (x : ℚ) (y : ℚ).

Русский

Для x,y ∈ ℚ≥0 отображение в ℚ сохраняет максимум: (max x y)↑ = max (x↑) (y↑).

LaTeX

$$$\bigl(\max(x,y) : \mathbb{Q}_{\ge 0}\bigr)^{\uparrow} = \max\bigl(x^{\uparrow}, y^{\uparrow}\bigr).$$$

Lean4

@[norm_cast]
theorem coe_max (x y : ℚ≥0) : ((max x y : ℚ≥0) : ℚ) = max (x : ℚ) (y : ℚ) :=
  coe_mono.map_max

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