Source indexedlemma · leanprover/lean4:v4.32.0

ENNReal.toReal_Ioo_eq_Ioo

Carleson.ToMathlib.MeasureTheory.Measure.NNReal · Carleson/ToMathlib/MeasureTheory/Measure/NNReal.lean:332 to 346

Mathematical statement

Exact Lean statement

lemma ENNReal.toReal_Ioo_eq_Ioo {a b : ℝ≥0∞} (ha : a ≠ ∞) (hb : b ≠ ∞) :
    ENNReal.toReal '' Set.Ioo a b = Set.Ioo a.toReal b.toReal

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma ENNReal.toReal_Ioo_eq_Ioo {a b : ℝ≥0∞} (ha : a ≠ ∞) (hb : b ≠ ∞) :    ENNReal.toReal '' Set.Ioo a b = Set.Ioo a.toReal b.toReal := by  ext x  simp only [mem_image, mem_Ioo]  constructor  · rintro ⟨y, ⟨hy₁, hy₂⟩, hyx⟩    rw [← hyx]    constructor <;> gcongr    · finiteness  · rintro hx    use ENNReal.ofReal x    constructor    · rwa [lt_ofReal_iff_toReal_lt ha, ofReal_lt_iff_lt_toReal (le_trans toReal_nonneg hx.1.le) hb]    · rw [toReal_ofReal_eq_iff]      exact (le_trans toReal_nonneg hx.1.le)