Source indexedlemma · leanprover/lean4:v4.32.0

annulus_real_eq

Carleson.Classical.CarlesonOperatorReal · Carleson/Classical/CarlesonOperatorReal.lean:20 to 30

Mathematical statement

Exact Lean statement

lemma annulus_real_eq {x r R : ℝ} (r_nonneg : 0 ≤ r) : {y | dist x y ∈ Set.Ioo r R} = Set.Ioo (x - R) (x - r) ∪ Set.Ioo (x + r) (x + R)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma annulus_real_eq {x r R : ℝ} (r_nonneg : 0 ≤ r) : {y | dist x y ∈ Set.Ioo r R} = Set.Ioo (x - R) (x - r) ∪ Set.Ioo (x + r) (x + R) := by  ext y  simp only [Real.dist_eq, Set.mem_Ioo, lt_abs, neg_sub, abs_lt, neg_lt_sub_iff_lt_add,    Set.mem_setOf_eq, Set.mem_union]  constructor  · rintro ⟨(h₀ | h₀), h₁, h₂⟩    · left; constructor <;> linarith    · right; constructor <;> linarith  · rintro (⟨h₀, h₁⟩ | ⟨h₀, h₁⟩)    · exact ⟨by left; linarith, by constructor <;> linarith⟩    · exact ⟨by right; linarith, by constructor <;> linarith⟩