toNNReal_sSup — Mathlib

English

If all r ∈ s satisfy r ≠ ∞, then (sSup s).toNNReal = sSup (ENNReal.toNNReal '' s).

Русский

Пусть все r ∈ s удовлетворяют r ≠ ∞; тогда (sSup s).toNNReal = sSup (ENNReal.toNNReal '' s).

LaTeX

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

Lean4

theorem toNNReal_sSup (s : Set ℝ≥0∞) (hs : ∀ r ∈ s, r ≠ ∞) : (sSup s).toNNReal = sSup (ENNReal.toNNReal '' s) :=
  by
  have hf : ∀ i, ((↑) : s → ℝ≥0∞) i ≠ ∞ := fun ⟨r, rs⟩ => hs r rs
  simpa only [← sSup_range, ← image_eq_range, Subtype.range_coe_subtype] using (toNNReal_iSup hf)

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