English
The real value of the infimum equals the infimum of real values, for finite arguments.
Русский
Действительное значение инфимума равно инфимума действительных значений при конечных аргументах.
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_inf {a b : ℝ≥0∞} : a ≠ ∞ → b ≠ ∞ → (a ⊓ b).toReal = a.toReal ⊓ b.toReal :=
toReal_min