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