toReal_sSup — Mathlib

English

For a set s with no ∞, toReal of the supremum equals the supremum of the toReal-images: (sSup s).toReal = sSup (ENNReal.toReal '' s).

Русский

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

LaTeX

$$$ (\mathrm{sSup}\ s).toReal = \mathrm{sSup}\bigl( \mathrm{ENNReal.toReal} '' s \bigr) $$$

Lean4

theorem toReal_sSup (s : Set ℝ≥0∞) (hf : ∀ r ∈ s, r ≠ ∞) : (sSup s).toReal = sSup (ENNReal.toReal '' s) := by
  simp only [ENNReal.toReal, toNNReal_sSup s hf, NNReal.coe_sSup, Set.image_image]

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