coe_min — Mathlib

English

For x,y in the nonnegative rationals, the natural cast of min(x,y) equals the minimum of the casts: ((min x y : ℚ≥0) : ℚ) = min (x : ℚ) (y : ℚ).

Русский

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

LaTeX

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

Lean4

@[norm_cast]
theorem coe_min (x y : ℚ≥0) : ((min x y : ℚ≥0) : ℚ) = min (x : ℚ) (y : ℚ) :=
  coe_mono.map_min

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