Source indexedlemma · leanprover/lean4:v4.32.0

ENNReal.toReal_Iio_eq_Ico

Carleson.ToMathlib.MeasureTheory.Measure.NNReal · Carleson/ToMathlib/MeasureTheory/Measure/NNReal.lean:286 to 300

Mathematical statement

Exact Lean statement

lemma ENNReal.toReal_Iio_eq_Ico {a : ℝ≥0∞} (ha : a ≠ ∞) :
    ENNReal.toReal '' Set.Iio a = Set.Ico 0 a.toReal

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma ENNReal.toReal_Iio_eq_Ico {a : ℝ≥0∞} (ha : a ≠ ∞) :    ENNReal.toReal '' Set.Iio a = Set.Ico 0 a.toReal := by  ext x  simp only [mem_image, mem_Iio, mem_Ico]  constructor  · rintro ⟨y, ⟨hy₁, hy₂⟩⟩    rw [← hy₂]    constructor    · simp    · exact (ENNReal.toReal_lt_toReal hy₁.ne_top ha).mpr hy₁  · rintro ⟨zero_le_x, x_lt⟩    use ENNReal.ofReal x    constructor    · exact (ENNReal.ofReal_lt_iff_lt_toReal zero_le_x ha).mpr x_lt    · simpa