toReal_sup — Mathlib

English

The real value of the supremum equals the supremum 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}(\\max(a,b)) = \\max(\\operatorname{toReal}(a), \\operatorname{toReal}(b)). $$$$

Lean4

theorem toReal_sup {a b : ℝ≥0∞} : a ≠ ∞ → b ≠ ∞ → (a ⊔ b).toReal = a.toReal ⊔ b.toReal :=
  toReal_max

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