Source indexedlemma · leanprover/lean4:v4.32.0

ENNReal.toReal_Icc_eq_Icc

Carleson.ToMathlib.MeasureTheory.Measure.NNReal · Carleson/ToMathlib/MeasureTheory/Measure/NNReal.lean:315 to 329

Mathematical statement

Exact Lean statement

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

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma ENNReal.toReal_Icc_eq_Icc {a b : ℝ≥0∞} (ha : a ≠ ∞) (hb : b ≠ ∞) :    ENNReal.toReal '' Set.Icc a b = Set.Icc a.toReal b.toReal := by  ext x  simp only [mem_image, mem_Icc]  constructor  · rintro ⟨y, ⟨hy₁, hy₂⟩, hxy⟩    rw [← hxy]    constructor <;> gcongr    · exact ne_top_of_le_ne_top hb hy₂  · rintro hx    use ENNReal.ofReal x    constructor    · rwa [le_ofReal_iff_toReal_le ha (le_trans toReal_nonneg hx.1), ofReal_le_iff_le_toReal hb]    · rw [toReal_ofReal_eq_iff]      exact (le_trans toReal_nonneg hx.1)