toReal_sInf — Mathlib

English

For a set s of ENNReal numbers with no ∞ in s, the toReal of the infimum equals the infimum of the toReal-images: (sInf s).toReal = sInf (ENNReal.toReal '' s).

Русский

Для множества s ENNReal без ∞ выполняется: (sInf s).toReal = sInf (ENNReal.toReal '' s).

LaTeX

$$$ (\mathrm{sInf}\ s).toReal = \mathrm{sInf}\ (\mathrm{ENNReal.toReal} '' s) $$$

Lean4

theorem toReal_sInf (s : Set ℝ≥0∞) (hf : ∀ r ∈ s, r ≠ ∞) : (sInf s).toReal = sInf (ENNReal.toReal '' s) := by
  simp only [ENNReal.toReal, toNNReal_sInf s hf, NNReal.coe_sInf, Set.image_image]

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