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