English
The real value of the minimum equals the minimum of real values, provided neither argument is ∞.
Русский
Действительное значение минимума равно минимуму действительных значений, если ни один аргумент не бесконечен.
LaTeX
$$$$ \\forall a,b \\in \\mathbb{R}_{\\ge 0}^{\\infty},\\; a \\neq \\infty \\land b \\neq \\infty \\Rightarrow \\operatorname{toReal}(\\min(a,b)) = \\min(\\operatorname{toReal}(a), \\operatorname{toReal}(b)). $$$$
Lean4
theorem toReal_min {a b : ℝ≥0∞} (hr : a ≠ ∞) (hp : b ≠ ∞) :
ENNReal.toReal (min a b) = min (ENNReal.toReal a) (ENNReal.toReal b) :=
(le_total a b).elim (fun h => by simp only [h, ENNReal.toReal_mono hp h, min_eq_left]) fun h => by
simp only [h, ENNReal.toReal_mono hr h, min_eq_right]
