Source indexedlemma · leanprover/lean4:v4.32.0

Set.EAnnulus.cc_eq_annulus

Carleson.ToMathlib.Annulus · Carleson/ToMathlib/Annulus.lean:356 to 365

Mathematical statement

Exact Lean statement

lemma cc_eq_annulus {x : X} {r R : ℝ} (h : 0 < r ∨ 0 ≤ R) :
    cc x (ENNReal.ofReal r) (ENNReal.ofReal R) = Annulus.cc x r R

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma cc_eq_annulus {x : X} {r R : ℝ} (h : 0 < r ∨ 0 ≤ R) :    cc x (ENNReal.ofReal r) (ENNReal.ofReal R) = Annulus.cc x r R := by  by_cases hR : 0 ≤ R  · simp_rw [cc, Annulus.cc, edist_dist, mem_Icc, ENNReal.ofReal_le_ofReal_iff dist_nonneg,      ENNReal.ofReal_le_ofReal_iff hR]  have r0 := h.resolve_right hR  have R_lt_r := (lt_of_not_ge hR).trans r0  rw [Annulus.cc_eq_empty R_lt_r]  refine eq_empty_of_forall_notMem (fun y hy ↦ ?_)  exact not_le_of_gt ((ENNReal.ofReal_lt_ofReal_iff r0).mpr R_lt_r) (hy.1.trans hy.2)