Source indexedlemma · leanprover/lean4:v4.32.0

ENNReal.toReal_Ioi_eq_Ioi

Carleson.ToMathlib.MeasureTheory.Measure.NNReal · Carleson/ToMathlib/MeasureTheory/Measure/NNReal.lean:364 to 382

Mathematical statement

Exact Lean statement

lemma ENNReal.toReal_Ioi_eq_Ioi {a : ℝ≥0∞} (ha : a ≠ ∞) :
    ENNReal.toReal '' Set.Ioi a = Set.Ioi a.toReal ∪ {0}

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma ENNReal.toReal_Ioi_eq_Ioi {a : ℝ≥0∞} (ha : a ≠ ∞) :    ENNReal.toReal '' Set.Ioi a = Set.Ioi a.toReal ∪ {0} := by  ext x  simp only [mem_image, mem_Ioi, union_singleton, mem_insert_iff]  constructor  · rintro ⟨y, hy, hyx⟩    by_cases h : y = ⊤    · left      rw [← hyx, h, ENNReal.toReal_top]    right    rw [← hyx]    gcongr  · rintro (x_zero | hxa)    · exact ⟨⊤, by finiteness, by simp [x_zero]⟩    use ENNReal.ofReal x    simp only [toReal_ofReal_eq_iff]    constructor    · rwa [ENNReal.lt_ofReal_iff_toReal_lt ha]    · exact (le_trans toReal_nonneg hxa.le)