toReal_inf — Mathlib

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

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