Source indexedlemma · leanprover/lean4:v4.32.0

Set.EAnnulus.oc_eq_annulus

Carleson.ToMathlib.Annulus · Carleson/ToMathlib/Annulus.lean:340 to 349

Mathematical statement

Exact Lean statement

lemma oc_eq_annulus {x : X} {r R : ℝ} (hr : 0 ≤ r) :
    oc x (ENNReal.ofReal r) (ENNReal.ofReal R) = Annulus.oc x r R

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma oc_eq_annulus {x : X} {r R : ℝ} (hr : 0 ≤ r) :    oc x (ENNReal.ofReal r) (ENNReal.ofReal R) = Annulus.oc x r R := by  by_cases hR : 0 ≤ R  · simp_rw [oc, Annulus.oc, edist_dist, mem_Ioc, ENNReal.ofReal_lt_ofReal_iff_of_nonneg hr,      ENNReal.ofReal_le_ofReal_iff hR]  · have R_le_r := (lt_of_lt_of_le (lt_of_not_ge hR) hr).le    rw [Annulus.oc_eq_empty R_le_r]    -- future: can `ext y; push _ ∈ _` golf this, after sufficient `push` tagging?    refine eq_empty_of_forall_notMem (fun y hy ↦ ?_)    exact not_le_of_gt (lt_of_le_of_lt (ENNReal.ofReal_le_ofReal R_le_r) hy.1) hy.2