Source indexedlemma · leanprover/lean4:v4.32.0

ENNReal.toNNReal_Iio

Carleson.ToMathlib.MeasureTheory.Measure.NNReal · Carleson/ToMathlib/MeasureTheory/Measure/NNReal.lean:432 to 450

Mathematical statement

Exact Lean statement

lemma ENNReal.toNNReal_Iio {b : ℝ≥0∞} : ENNReal.toNNReal '' Set.Iio b
    = if b = ∞ then Set.univ else Set.Iio b.toNNReal

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma ENNReal.toNNReal_Iio {b : ℝ≥0∞} : ENNReal.toNNReal '' Set.Iio b    = if b = ∞ then Set.univ else Set.Iio b.toNNReal := by  split_ifs with hb  · rw [hb]    ext x    simp only [mem_image, mem_Iio, mem_univ, iff_true]    use ofNNReal x    simp  · ext x    simp only [mem_image, mem_Iio]    constructor    · rintro ⟨y, hyb, hyx⟩      rwa [← hyx, ENNReal.toNNReal_lt_toNNReal _ hb]      grind    · intro h      use ofNNReal x      simp only [toNNReal_coe, and_true]      rw [← ENNReal.toNNReal_lt_toNNReal (by simp) hb]      simpa