Source indexedlemma · leanprover/lean4:v4.32.0

ENNReal.ofReal_Iio_eq

Carleson.ToMathlib.MeasureTheory.Measure.NNReal · Carleson/ToMathlib/MeasureTheory/Measure/NNReal.lean:413 to 430

Mathematical statement

Exact Lean statement

lemma ENNReal.ofReal_Iio_eq {b : ℝ≥0∞} : ENNReal.ofReal ⁻¹' Set.Iio b
    = if b = 0 then ∅ else if b = ∞ then Set.univ else Set.Iio b.toReal

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma ENNReal.ofReal_Iio_eq {b : ℝ≥0∞} : ENNReal.ofReal ⁻¹' Set.Iio b    = if b = 0 then ∅ else if b = ∞ then Set.univ else Set.Iio b.toReal := by  split_ifs with hb hb'  · rw [hb]    simp  · rw [hb']    simp only [preimage_eq_univ_iff]    intro x hx    simp only [mem_Iio]    rcases hx with ⟨y, hy⟩    rw [← hy]    simp  · ext x    simp only [mem_preimage, mem_Iio]    by_cases! hx : x < 0    · rw [ENNReal.ofReal_of_nonpos hx.le]      exact ⟨fun _ ↦ hx.trans_le (by positivity), fun _ ↦ by positivity⟩    exact ofReal_lt_iff_lt_toReal hx hb'