Source indexedlemma · leanprover/lean4:v4.32.0

ENNReal.map_toReal_eq_map_toReal_comap_ofReal'

Carleson.ToMathlib.MeasureTheory.Measure.NNReal · Carleson/ToMathlib/MeasureTheory/Measure/NNReal.lean:49 to 67

Mathematical statement

Exact Lean statement

lemma ENNReal.map_toReal_eq_map_toReal_comap_ofReal' {s : Set ℝ≥0∞} (h : ∞ ∈ s) :
    ENNReal.toReal '' s = NNReal.toReal '' (ENNReal.ofNNReal ⁻¹' s) ∪ {0}

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma ENNReal.map_toReal_eq_map_toReal_comap_ofReal' {s : Set ℝ≥0∞} (h : ∞ ∈ s) :    ENNReal.toReal '' s = NNReal.toReal '' (ENNReal.ofNNReal ⁻¹' s) ∪ {0}:= by  ext x  simp only [mem_image]  constructor  · rintro ⟨y, hys, hyx⟩    by_cases hy : y = ∞    · rw [← hyx, hy]      simp    left    use y.toNNReal    simp only [mem_preimage]    rw [coe_toNNReal hy]    use hys    rwa [coe_toNNReal_eq_toReal]  · rintro (⟨y, hys, hyx⟩ | hx)    · use ENNReal.ofNNReal y, hys, hyx    · use ∞, h      simp only [toReal_top, hx.symm]