Annulus

In this file we define an annulus in a pseudometric space X to be a set consisting of all y such that dist x y lies in an interval between r and R. An annulus is defined for each type of interval (Ioo, Ioc, etc.) with a parallel naming scheme, except that we do not define annuli for Iio and Iic, as they would be balls.

We also define EAnnulus similarly using edist instead of dist.

Upstreaming status: ready; two style questions should be answered in the process (see below).

Tags

annulus, eannulus

Annulus

def Set.Annulus.oo {X : Type u_1} [PseudoMetricSpace X] (x : X) (r R : ℝ) : Set X

Equations

• Set.Annulus.oo x r R = {y : X | dist x y ∈ Set.Ioo r R}

def Set.Annulus.oc {X : Type u_1} [PseudoMetricSpace X] (x : X) (r R : ℝ) : Set X

Equations

• Set.Annulus.oc x r R = {y : X | dist x y ∈ Set.Ioc r R}

def Set.Annulus.co {X : Type u_1} [PseudoMetricSpace X] (x : X) (r R : ℝ) : Set X

Equations

• Set.Annulus.co x r R = {y : X | dist x y ∈ Set.Ico r R}

def Set.Annulus.cc {X : Type u_1} [PseudoMetricSpace X] (x : X) (r R : ℝ) : Set X

Equations

• Set.Annulus.cc x r R = {y : X | dist x y ∈ Set.Icc r R}

def Set.Annulus.oi {X : Type u_1} [PseudoMetricSpace X] (x : X) (r : ℝ) : Set X

Equations

• Set.Annulus.oi x r = {y : X | dist x y ∈ Set.Ioi r}

def Set.Annulus.ci {X : Type u_1} [PseudoMetricSpace X] (x : X) (r : ℝ) : Set X

Equations

• Set.Annulus.ci x r = {y : X | dist x y ∈ Set.Ici r}

theorem Set.Annulus.oo_eq {X : Type u_1} [PseudoMetricSpace X] {x : X} {r R : ℝ} : oo x r R = Metric.ball x R ∩ (Metric.closedBall x r)ᶜ

theorem Set.Annulus.oc_eq {X : Type u_1} [PseudoMetricSpace X] {x : X} {r R : ℝ} : oc x r R = Metric.closedBall x R ∩ (Metric.closedBall x r)ᶜ

theorem Set.Annulus.co_eq {X : Type u_1} [PseudoMetricSpace X] {x : X} {r R : ℝ} : co x r R = Metric.ball x R ∩ (Metric.ball x r)ᶜ

theorem Set.Annulus.cc_eq {X : Type u_1} [PseudoMetricSpace X] {x : X} {r R : ℝ} : cc x r R = Metric.closedBall x R ∩ (Metric.ball x r)ᶜ

theorem Set.Annulus.oi_eq {X : Type u_1} [PseudoMetricSpace X] {x : X} {r : ℝ} : oi x r = (Metric.closedBall x r)ᶜ

theorem Set.Annulus.ci_eq {X : Type u_1} [PseudoMetricSpace X] {x : X} {r : ℝ} : ci x r = (Metric.ball x r)ᶜ

@[simp]

theorem Set.Annulus.oo_eq_empty {X : Type u_1} [PseudoMetricSpace X] {x : X} {r R : ℝ} (h : R ≤ r) : oo x r R = ∅

@[simp]

theorem Set.Annulus.oc_eq_empty {X : Type u_1} [PseudoMetricSpace X] {x : X} {r R : ℝ} (h : R ≤ r) : oc x r R = ∅

@[simp]

theorem Set.Annulus.co_eq_empty {X : Type u_1} [PseudoMetricSpace X] {x : X} {r R : ℝ} (h : R ≤ r) : co x r R = ∅

@[simp]

theorem Set.Annulus.cc_eq_empty {X : Type u_1} [PseudoMetricSpace X] {x : X} {r R : ℝ} (h : R < r) : cc x r R = ∅

theorem Set.Annulus.oo_subset_oo {X : Type u_1} [PseudoMetricSpace X] {x : X} {r₁ R₁ r₂ R₂ : ℝ} (hr : r₂ ≤ r₁) (hR : R₁ ≤ R₂) : oo x r₁ R₁ ⊆ oo x r₂ R₂

theorem Set.Annulus.oo_subset_oc {X : Type u_1} [PseudoMetricSpace X] {x : X} {r₁ R₁ r₂ R₂ : ℝ} (hr : r₂ ≤ r₁) (hR : R₁ ≤ R₂) : oo x r₁ R₁ ⊆ oc x r₂ R₂

theorem Set.Annulus.oo_subset_co {X : Type u_1} [PseudoMetricSpace X] {x : X} {r₁ R₁ r₂ R₂ : ℝ} (hr : r₂ ≤ r₁) (hR : R₁ ≤ R₂) : oo x r₁ R₁ ⊆ co x r₂ R₂

theorem Set.Annulus.oo_subset_cc {X : Type u_1} [PseudoMetricSpace X] {x : X} {r₁ R₁ r₂ R₂ : ℝ} (hr : r₂ ≤ r₁) (hR : R₁ ≤ R₂) : oo x r₁ R₁ ⊆ cc x r₂ R₂

theorem Set.Annulus.oo_subset_oi {X : Type u_1} [PseudoMetricSpace X] {x : X} {r₁ R₁ r₂ : ℝ} (hr : r₂ ≤ r₁) : oo x r₁ R₁ ⊆ oi x r₂

theorem Set.Annulus.oo_subset_ci {X : Type u_1} [PseudoMetricSpace X] {x : X} {r₁ R₁ r₂ : ℝ} (hr : r₂ ≤ r₁) : oo x r₁ R₁ ⊆ ci x r₂

theorem Set.Annulus.oc_subset_oo {X : Type u_1} [PseudoMetricSpace X] {x : X} {r₁ R₁ r₂ R₂ : ℝ} (hr : r₂ ≤ r₁) (hR : R₁ < R₂) : oc x r₁ R₁ ⊆ oo x r₂ R₂

theorem Set.Annulus.oc_subset_oc {X : Type u_1} [PseudoMetricSpace X] {x : X} {r₁ R₁ r₂ R₂ : ℝ} (hr : r₂ ≤ r₁) (hR : R₁ ≤ R₂) : oc x r₁ R₁ ⊆ oc x r₂ R₂

theorem Set.Annulus.oc_subset_co {X : Type u_1} [PseudoMetricSpace X] {x : X} {r₁ R₁ r₂ R₂ : ℝ} (hr : r₂ ≤ r₁) (hR : R₁ < R₂) : oc x r₁ R₁ ⊆ co x r₂ R₂

theorem Set.Annulus.oc_subset_cc {X : Type u_1} [PseudoMetricSpace X] {x : X} {r₁ R₁ r₂ R₂ : ℝ} (hr : r₂ ≤ r₁) (hR : R₁ ≤ R₂) : oc x r₁ R₁ ⊆ cc x r₂ R₂

theorem Set.Annulus.oc_subset_oi {X : Type u_1} [PseudoMetricSpace X] {x : X} {r₁ R₁ r₂ : ℝ} (hr : r₂ ≤ r₁) : oo x r₁ R₁ ⊆ oi x r₂

theorem Set.Annulus.oc_subset_ci {X : Type u_1} [PseudoMetricSpace X] {x : X} {r₁ R₁ r₂ : ℝ} (hr : r₂ ≤ r₁) : oc x r₁ R₁ ⊆ ci x r₂

theorem Set.Annulus.co_subset_oo {X : Type u_1} [PseudoMetricSpace X] {x : X} {r₁ R₁ r₂ R₂ : ℝ} (hr : r₂ < r₁) (hR : R₁ ≤ R₂) : co x r₁ R₁ ⊆ oo x r₂ R₂

theorem Set.Annulus.co_subset_oc {X : Type u_1} [PseudoMetricSpace X] {x : X} {r₁ R₁ r₂ R₂ : ℝ} (hr : r₂ < r₁) (hR : R₁ ≤ R₂) : co x r₁ R₁ ⊆ oc x r₂ R₂

theorem Set.Annulus.co_subset_co {X : Type u_1} [PseudoMetricSpace X] {x : X} {r₁ R₁ r₂ R₂ : ℝ} (hr : r₂ ≤ r₁) (hR : R₁ ≤ R₂) : co x r₁ R₁ ⊆ co x r₂ R₂

theorem Set.Annulus.co_subset_cc {X : Type u_1} [PseudoMetricSpace X] {x : X} {r₁ R₁ r₂ R₂ : ℝ} (hr : r₂ ≤ r₁) (hR : R₁ ≤ R₂) : co x r₁ R₁ ⊆ cc x r₂ R₂

theorem Set.Annulus.co_subset_oi {X : Type u_1} [PseudoMetricSpace X] {x : X} {r₁ R₁ r₂ : ℝ} (hr : r₂ < r₁) : co x r₁ R₁ ⊆ oi x r₂

theorem Set.Annulus.co_subset_ci {X : Type u_1} [PseudoMetricSpace X] {x : X} {r₁ R₁ r₂ : ℝ} (hr : r₂ ≤ r₁) : co x r₁ R₁ ⊆ ci x r₂

theorem Set.Annulus.cc_subset_oo {X : Type u_1} [PseudoMetricSpace X] {x : X} {r₁ R₁ r₂ R₂ : ℝ} (hr : r₂ < r₁) (hR : R₁ < R₂) : cc x r₁ R₁ ⊆ oo x r₂ R₂

theorem Set.Annulus.cc_subset_oc {X : Type u_1} [PseudoMetricSpace X] {x : X} {r₁ R₁ r₂ R₂ : ℝ} (hr : r₂ < r₁) (hR : R₁ ≤ R₂) : cc x r₁ R₁ ⊆ oc x r₂ R₂

theorem Set.Annulus.cc_subset_co {X : Type u_1} [PseudoMetricSpace X] {x : X} {r₁ R₁ r₂ R₂ : ℝ} (hr : r₂ ≤ r₁) (hR : R₁ < R₂) : cc x r₁ R₁ ⊆ co x r₂ R₂

theorem Set.Annulus.cc_subset_cc {X : Type u_1} [PseudoMetricSpace X] {x : X} {r₁ R₁ r₂ R₂ : ℝ} (hr : r₂ ≤ r₁) (hR : R₁ ≤ R₂) : cc x r₁ R₁ ⊆ cc x r₂ R₂

theorem Set.Annulus.cc_subset_oi {X : Type u_1} [PseudoMetricSpace X] {x : X} {r₁ R₁ r₂ : ℝ} (hr : r₂ < r₁) : cc x r₁ R₁ ⊆ oi x r₂

theorem Set.Annulus.cc_subset_ci {X : Type u_1} [PseudoMetricSpace X] {x : X} {r₁ R₁ r₂ : ℝ} (hr : r₂ ≤ r₁) : cc x r₁ R₁ ⊆ ci x r₂

theorem Set.Annulus.oo_subset_ball {X : Type u_1} [PseudoMetricSpace X] {x : X} {r R : ℝ} : oo x r R ⊆ Metric.ball x R

theorem Set.Annulus.oc_subset_closedBall {X : Type u_1} [PseudoMetricSpace X] {x : X} {r R : ℝ} : oc x r R ⊆ Metric.closedBall x R

theorem Set.Annulus.co_subset_ball {X : Type u_1} [PseudoMetricSpace X] {x : X} {r R : ℝ} : co x r R ⊆ Metric.ball x R

theorem Set.Annulus.cc_subset_closedBall {X : Type u_1} [PseudoMetricSpace X] {x : X} {r R : ℝ} : cc x r R ⊆ Metric.closedBall x R

@[simp]

theorem Set.Annulus.oc_union_oo {X : Type u_1} [PseudoMetricSpace X] {x : X} {r r' R : ℝ} (h₁ : r ≤ r') (h₂ : r' < R) : oc x r r' ∪ oo x r' R = oo x r R

@[simp]

theorem Set.Annulus.oc_union_oc {X : Type u_1} [PseudoMetricSpace X] {x : X} {r r' R : ℝ} (h₁ : r ≤ r') (h₂ : r' ≤ R) : oc x r r' ∪ oc x r' R = oc x r R

@[simp]

theorem Set.Annulus.oo_union_co {X : Type u_1} [PseudoMetricSpace X] {x : X} {r r' R : ℝ} (h₁ : r < r') (h₂ : r' ≤ R) : oo x r r' ∪ co x r' R = oo x r R

@[simp]

theorem Set.Annulus.oo_union_cc {X : Type u_1} [PseudoMetricSpace X] {x : X} {r r' R : ℝ} (h₁ : r < r') (h₂ : r' ≤ R) : oo x r r' ∪ cc x r' R = oc x r R

@[simp]

theorem Set.Annulus.cc_union_oo {X : Type u_1} [PseudoMetricSpace X] {x : X} {r r' R : ℝ} (h₁ : r ≤ r') (h₂ : r' < R) : cc x r r' ∪ oo x r' R = co x r R

@[simp]

theorem Set.Annulus.cc_union_oc {X : Type u_1} [PseudoMetricSpace X] {x : X} {r r' R : ℝ} (h₁ : r ≤ r') (h₂ : r' ≤ R) : cc x r r' ∪ oc x r' R = cc x r R

@[simp]

theorem Set.Annulus.co_union_co {X : Type u_1} [PseudoMetricSpace X] {x : X} {r r' R : ℝ} (h₁ : r ≤ r') (h₂ : r' ≤ R) : co x r r' ∪ co x r' R = co x r R

@[simp]

theorem Set.Annulus.co_union_cc {X : Type u_1} [PseudoMetricSpace X] {x : X} {r r' R : ℝ} (h₁ : r ≤ r') (h₂ : r' ≤ R) : co x r r' ∪ cc x r' R = cc x r R

@[simp]

theorem Set.Annulus.oc_union_oi {X : Type u_1} [PseudoMetricSpace X] {x : X} {r R : ℝ} (h : r ≤ R) : oc x r R ∪ oi x R = oi x r

@[simp]

theorem Set.Annulus.oo_union_ci {X : Type u_1} [PseudoMetricSpace X] {x : X} {r R : ℝ} (h : r < R) : oo x r R ∪ ci x R = oi x r

@[simp]

theorem Set.Annulus.cc_union_oi {X : Type u_1} [PseudoMetricSpace X] {x : X} {r R : ℝ} (h : r ≤ R) : cc x r R ∪ oi x R = ci x r

@[simp]

theorem Set.Annulus.co_union_ci {X : Type u_1} [PseudoMetricSpace X] {x : X} {r R : ℝ} (h : r ≤ R) : co x r R ∪ ci x R = ci x r

theorem Set.Annulus.biUnion_Ici_co_map_succ {X : Type u_1} [PseudoMetricSpace X] {α : Type u_2} [LinearOrder α] [SuccOrder α] [IsSuccArchimedean α] {x : X} {f : α → ℝ} {a : α} (hf : ∀ i ∈ Ici a, f a ≤ f i) (h2f : ¬BddAbove (f '' Ici a)) : ⋃ i ∈ Ici a, co x (f i) (f (Order.succ i)) = ci x (f a)

Union formula for Set.Annulus.co x (f i) (f (Order.succ i)) over i ∈ Ici a. See also iUnion_co_map_succ_eq_ci for the specialization a = ⊥.

theorem Set.Annulus.biUnion_Ici_oc_map_succ {X : Type u_1} [PseudoMetricSpace X] {α : Type u_2} [LinearOrder α] [SuccOrder α] [IsSuccArchimedean α] {x : X} {f : α → ℝ} {a : α} (hf : ∀ i ∈ Ici a, f a ≤ f i) (h2f : ¬BddAbove (f '' Ici a)) : ⋃ i ∈ Ici a, oc x (f i) (f (Order.succ i)) = oi x (f a)

Union formula for Set.Annulus.oc x (f i) (f (Order.succ i)) over i ∈ Ici a. See also iUnion_oc_map_succ_eq_oi for the specialization a = ⊥.

theorem Set.Annulus.iUnion_co_map_succ_eq_ci {X : Type u_1} [PseudoMetricSpace X] {α : Type u_2} [LinearOrder α] [OrderBot α] [SuccOrder α] [IsSuccArchimedean α] {x : X} {f : α → ℝ} (hf : ∀ (a : α), f ⊥ ≤ f a) (h2f : ¬BddAbove (range f)) : ⋃ (a : α), co x (f a) (f (Order.succ a)) = ci x (f ⊥)

Special case a = ⊥ of biUnion_Ici_co_map_succ.

theorem Set.Annulus.iUnion_oc_map_succ_eq_oi {X : Type u_1} [PseudoMetricSpace X] {α : Type u_2} [LinearOrder α] [OrderBot α] [SuccOrder α] [IsSuccArchimedean α] {x : X} {f : α → ℝ} (hf : ∀ (a : α), f ⊥ ≤ f a) (h2f : ¬BddAbove (range f)) : ⋃ (a : α), oc x (f a) (f (Order.succ a)) = oi x (f ⊥)

Special case a = ⊥ of biUnion_Ici_oc_map_succ.

theorem Set.Annulus.pairwise_disjoint_on_co_succ {X : Type u_1} [PseudoMetricSpace X] {ι : Type u_3} [LinearOrder ι] [SuccOrder ι] {x : X} {f : ι → ℝ} (hf : Monotone f) : Pairwise (Function.onFun Disjoint fun (i : ι) => co x (f i) (f (Order.succ i)))

theorem Set.Annulus.pairwise_disjoint_on_oc_succ {X : Type u_1} [PseudoMetricSpace X] {ι : Type u_3} [LinearOrder ι] [SuccOrder ι] {x : X} {f : ι → ℝ} (hf : Monotone f) : Pairwise (Function.onFun Disjoint fun (i : ι) => oc x (f i) (f (Order.succ i)))

theorem Set.Annulus.measurableSet_oo {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] {x : X} {r R : ℝ} : MeasurableSet (oo x r R)

theorem Set.Annulus.measurableSet_oc {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] {x : X} {r R : ℝ} : MeasurableSet (oc x r R)

theorem Set.Annulus.measurableSet_co {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] {x : X} {r R : ℝ} : MeasurableSet (co x r R)

theorem Set.Annulus.measurableSet_cc {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] {x : X} {r R : ℝ} : MeasurableSet (cc x r R)

theorem Set.Annulus.measurableSet_oi {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] {x : X} {r : ℝ} : MeasurableSet (oi x r)

theorem Set.Annulus.measurableSet_ci {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] {x : X} {r : ℝ} : MeasurableSet (ci x r)

EAnnulus

def Set.EAnnulus.oo {X : Type u_1} [PseudoMetricSpace X] (x : X) (r R : ENNReal) : Set X

Equations

• Set.EAnnulus.oo x r R = {y : X | edist x y ∈ Set.Ioo r R}

def Set.EAnnulus.oc {X : Type u_1} [PseudoMetricSpace X] (x : X) (r R : ENNReal) : Set X

Equations

• Set.EAnnulus.oc x r R = {y : X | edist x y ∈ Set.Ioc r R}

def Set.EAnnulus.co {X : Type u_1} [PseudoMetricSpace X] (x : X) (r R : ENNReal) : Set X

Equations

• Set.EAnnulus.co x r R = {y : X | edist x y ∈ Set.Ico r R}

def Set.EAnnulus.cc {X : Type u_1} [PseudoMetricSpace X] (x : X) (r R : ENNReal) : Set X

Equations

• Set.EAnnulus.cc x r R = {y : X | edist x y ∈ Set.Icc r R}

def Set.EAnnulus.oi {X : Type u_1} [PseudoMetricSpace X] (x : X) (r : ENNReal) : Set X

Equations

• Set.EAnnulus.oi x r = {y : X | edist x y ∈ Set.Ioi r}

def Set.EAnnulus.ci {X : Type u_1} [PseudoMetricSpace X] (x : X) (r : ENNReal) : Set X

Equations

• Set.EAnnulus.ci x r = {y : X | edist x y ∈ Set.Ici r}

theorem Set.EAnnulus.oo_eq_annulus {X : Type u_1} [PseudoMetricSpace X] {x : X} {r R : ℝ} (hr : 0 ≤ r) : oo x (ENNReal.ofReal r) (ENNReal.ofReal R) = Annulus.oo x r R

theorem Set.EAnnulus.oc_eq_annulus {X : Type u_1} [PseudoMetricSpace X] {x : X} {r R : ℝ} (hr : 0 ≤ r) : oc x (ENNReal.ofReal r) (ENNReal.ofReal R) = Annulus.oc x r R

theorem Set.EAnnulus.co_eq_annulus {X : Type u_1} [PseudoMetricSpace X] {x : X} {r R : ℝ} : co x (ENNReal.ofReal r) (ENNReal.ofReal R) = Annulus.co x r R

theorem Set.EAnnulus.cc_eq_annulus {X : Type u_1} [PseudoMetricSpace X] {x : X} {r R : ℝ} (h : 0 < r ∨ 0 ≤ R) : cc x (ENNReal.ofReal r) (ENNReal.ofReal R) = Annulus.cc x r R

theorem Set.EAnnulus.oi_eq_annulus {X : Type u_1} [PseudoMetricSpace X] {x : X} {r : ℝ} (hr : 0 ≤ r) : oi x (ENNReal.ofReal r) = Annulus.oi x r

theorem Set.EAnnulus.ci_eq_annulus {X : Type u_1} [PseudoMetricSpace X] {x : X} {r : ℝ} : ci x (ENNReal.ofReal r) = Annulus.ci x r

theorem Set.EAnnulus.oo_eq_of_lt_top {X : Type u_1} [PseudoMetricSpace X] {x : X} {r R : ENNReal} (hr : r < ⊤) (hR : R < ⊤) : oo x r R = Metric.ball x R.toReal ∩ (Metric.closedBall x r.toReal)ᶜ

theorem Set.EAnnulus.oc_eq_of_lt_top {X : Type u_1} [PseudoMetricSpace X] {x : X} {r R : ENNReal} (hr : r < ⊤) (hR : R < ⊤) : oc x r R = Metric.closedBall x R.toReal ∩ (Metric.closedBall x r.toReal)ᶜ

theorem Set.EAnnulus.co_eq_of_lt_top {X : Type u_1} [PseudoMetricSpace X] {x : X} {r R : ENNReal} (hr : r < ⊤) (hR : R < ⊤) : co x r R = Metric.ball x R.toReal ∩ (Metric.ball x r.toReal)ᶜ

theorem Set.EAnnulus.cc_eq_of_lt_top {X : Type u_1} [PseudoMetricSpace X] {x : X} {r R : ENNReal} (hr : r < ⊤) (hR : R < ⊤) : cc x r R = Metric.closedBall x R.toReal ∩ (Metric.ball x r.toReal)ᶜ

theorem Set.EAnnulus.oi_eq_of_lt_top {X : Type u_1} [PseudoMetricSpace X] {x : X} {r : ENNReal} (hr : r < ⊤) : oi x r = (Metric.closedBall x r.toReal)ᶜ

theorem Set.EAnnulus.ci_eq_of_lt_top {X : Type u_1} [PseudoMetricSpace X] {x : X} {r : ENNReal} (hr : r < ⊤) : ci x r = (Metric.ball x r.toReal)ᶜ

@[simp]

theorem Set.EAnnulus.oo_eq_empty {X : Type u_1} [PseudoMetricSpace X] {x : X} {r R : ENNReal} (h : R ≤ r) : oo x r R = ∅

@[simp]

theorem Set.EAnnulus.oc_eq_empty {X : Type u_1} [PseudoMetricSpace X] {x : X} {r R : ENNReal} (h : R ≤ r) : oc x r R = ∅

@[simp]

theorem Set.EAnnulus.co_eq_empty {X : Type u_1} [PseudoMetricSpace X] {x : X} {r R : ENNReal} (h : R ≤ r) : co x r R = ∅

@[simp]

theorem Set.EAnnulus.cc_eq_empty {X : Type u_1} [PseudoMetricSpace X] {x : X} {r R : ENNReal} (h : R < r) : cc x r R = ∅

@[simp]

theorem Set.EAnnulus.cc_top_eq_empty {X : Type u_1} [PseudoMetricSpace X] {x : X} {R : ENNReal} : cc x ⊤ R = ∅

@[simp]

theorem Set.EAnnulus.oi_eq_empty {X : Type u_1} [PseudoMetricSpace X] {x : X} : oi x ⊤ = ∅

@[simp]

theorem Set.EAnnulus.ci_eq_empty {X : Type u_1} [PseudoMetricSpace X] {x : X} : ci x ⊤ = ∅

theorem Set.EAnnulus.oo_eq_of_top {X : Type u_1} [PseudoMetricSpace X] {x : X} {r : ENNReal} (hr : r < ⊤) : oo x r ⊤ = (Metric.closedBall x r.toReal)ᶜ

theorem Set.EAnnulus.oc_eq_of_top {X : Type u_1} [PseudoMetricSpace X] {x : X} {r : ENNReal} (hr : r < ⊤) : oc x r ⊤ = (Metric.closedBall x r.toReal)ᶜ

theorem Set.EAnnulus.co_eq_of_top {X : Type u_1} [PseudoMetricSpace X] {x : X} {r : ENNReal} (hr : r < ⊤) : co x r ⊤ = (Metric.ball x r.toReal)ᶜ

theorem Set.EAnnulus.cc_eq_of_top {X : Type u_1} [PseudoMetricSpace X] {x : X} {r : ENNReal} (hr : r < ⊤) : cc x r ⊤ = (Metric.ball x r.toReal)ᶜ

theorem Set.EAnnulus.oo_subset_oo {X : Type u_1} [PseudoMetricSpace X] {x : X} {r₁ R₁ r₂ R₂ : ENNReal} (hr : r₂ ≤ r₁) (hR : R₁ ≤ R₂) : oo x r₁ R₁ ⊆ oo x r₂ R₂

theorem Set.EAnnulus.oo_subset_oc {X : Type u_1} [PseudoMetricSpace X] {x : X} {r₁ R₁ r₂ R₂ : ENNReal} (hr : r₂ ≤ r₁) (hR : R₁ ≤ R₂) : oo x r₁ R₁ ⊆ oc x r₂ R₂

theorem Set.EAnnulus.oo_subset_co {X : Type u_1} [PseudoMetricSpace X] {x : X} {r₁ R₁ r₂ R₂ : ENNReal} (hr : r₂ ≤ r₁) (hR : R₁ ≤ R₂) : oo x r₁ R₁ ⊆ co x r₂ R₂

theorem Set.EAnnulus.oo_subset_cc {X : Type u_1} [PseudoMetricSpace X] {x : X} {r₁ R₁ r₂ R₂ : ENNReal} (hr : r₂ ≤ r₁) (hR : R₁ ≤ R₂) : oo x r₁ R₁ ⊆ cc x r₂ R₂

theorem Set.EAnnulus.oo_subset_oi {X : Type u_1} [PseudoMetricSpace X] {x : X} {r₁ R₁ r₂ : ENNReal} (hr : r₂ ≤ r₁) : oo x r₁ R₁ ⊆ oi x r₂

theorem Set.EAnnulus.oo_subset_ci {X : Type u_1} [PseudoMetricSpace X] {x : X} {r₁ R₁ r₂ : ENNReal} (hr : r₂ ≤ r₁) : oo x r₁ R₁ ⊆ ci x r₂

theorem Set.EAnnulus.oc_subset_oo {X : Type u_1} [PseudoMetricSpace X] {x : X} {r₁ R₁ r₂ R₂ : ENNReal} (hr : r₂ ≤ r₁) (hR : R₁ < R₂) : oc x r₁ R₁ ⊆ oo x r₂ R₂

theorem Set.EAnnulus.oc_subset_oc {X : Type u_1} [PseudoMetricSpace X] {x : X} {r₁ R₁ r₂ R₂ : ENNReal} (hr : r₂ ≤ r₁) (hR : R₁ ≤ R₂) : oc x r₁ R₁ ⊆ oc x r₂ R₂

theorem Set.EAnnulus.oc_subset_co {X : Type u_1} [PseudoMetricSpace X] {x : X} {r₁ R₁ r₂ R₂ : ENNReal} (hr : r₂ ≤ r₁) (hR : R₁ < R₂) : oc x r₁ R₁ ⊆ co x r₂ R₂

theorem Set.EAnnulus.oc_subset_cc {X : Type u_1} [PseudoMetricSpace X] {x : X} {r₁ R₁ r₂ R₂ : ENNReal} (hr : r₂ ≤ r₁) (hR : R₁ ≤ R₂) : oc x r₁ R₁ ⊆ cc x r₂ R₂

theorem Set.EAnnulus.oc_subset_oi {X : Type u_1} [PseudoMetricSpace X] {x : X} {r₁ R₁ r₂ : ENNReal} (hr : r₂ ≤ r₁) : oo x r₁ R₁ ⊆ oi x r₂

theorem Set.EAnnulus.oc_subset_ci {X : Type u_1} [PseudoMetricSpace X] {x : X} {r₁ R₁ r₂ : ENNReal} (hr : r₂ ≤ r₁) : oc x r₁ R₁ ⊆ ci x r₂

theorem Set.EAnnulus.co_subset_oo {X : Type u_1} [PseudoMetricSpace X] {x : X} {r₁ R₁ r₂ R₂ : ENNReal} (hr : r₂ < r₁) (hR : R₁ ≤ R₂) : co x r₁ R₁ ⊆ oo x r₂ R₂

theorem Set.EAnnulus.co_subset_oc {X : Type u_1} [PseudoMetricSpace X] {x : X} {r₁ R₁ r₂ R₂ : ENNReal} (hr : r₂ < r₁) (hR : R₁ ≤ R₂) : co x r₁ R₁ ⊆ oc x r₂ R₂

theorem Set.EAnnulus.co_subset_co {X : Type u_1} [PseudoMetricSpace X] {x : X} {r₁ R₁ r₂ R₂ : ENNReal} (hr : r₂ ≤ r₁) (hR : R₁ ≤ R₂) : co x r₁ R₁ ⊆ co x r₂ R₂

theorem Set.EAnnulus.co_subset_cc {X : Type u_1} [PseudoMetricSpace X] {x : X} {r₁ R₁ r₂ R₂ : ENNReal} (hr : r₂ ≤ r₁) (hR : R₁ ≤ R₂) : co x r₁ R₁ ⊆ cc x r₂ R₂

theorem Set.EAnnulus.co_subset_oi {X : Type u_1} [PseudoMetricSpace X] {x : X} {r₁ R₁ r₂ : ENNReal} (hr : r₂ < r₁) : co x r₁ R₁ ⊆ oi x r₂

theorem Set.EAnnulus.co_subset_ci {X : Type u_1} [PseudoMetricSpace X] {x : X} {r₁ R₁ r₂ : ENNReal} (hr : r₂ ≤ r₁) : co x r₁ R₁ ⊆ ci x r₂

theorem Set.EAnnulus.cc_subset_oo {X : Type u_1} [PseudoMetricSpace X] {x : X} {r₁ R₁ r₂ R₂ : ENNReal} (hr : r₂ < r₁) (hR : R₁ < R₂) : cc x r₁ R₁ ⊆ oo x r₂ R₂

theorem Set.EAnnulus.cc_subset_oc {X : Type u_1} [PseudoMetricSpace X] {x : X} {r₁ R₁ r₂ R₂ : ENNReal} (hr : r₂ < r₁) (hR : R₁ ≤ R₂) : cc x r₁ R₁ ⊆ oc x r₂ R₂

theorem Set.EAnnulus.cc_subset_co {X : Type u_1} [PseudoMetricSpace X] {x : X} {r₁ R₁ r₂ R₂ : ENNReal} (hr : r₂ ≤ r₁) (hR : R₁ < R₂) : cc x r₁ R₁ ⊆ co x r₂ R₂

theorem Set.EAnnulus.cc_subset_cc {X : Type u_1} [PseudoMetricSpace X] {x : X} {r₁ R₁ r₂ R₂ : ENNReal} (hr : r₂ ≤ r₁) (hR : R₁ ≤ R₂) : cc x r₁ R₁ ⊆ cc x r₂ R₂

theorem Set.EAnnulus.cc_subset_oi {X : Type u_1} [PseudoMetricSpace X] {x : X} {r₁ R₁ r₂ : ENNReal} (hr : r₂ < r₁) : cc x r₁ R₁ ⊆ oi x r₂

theorem Set.EAnnulus.cc_subset_ci {X : Type u_1} [PseudoMetricSpace X] {x : X} {r₁ R₁ r₂ : ENNReal} (hr : r₂ ≤ r₁) : cc x r₁ R₁ ⊆ ci x r₂

@[simp]

theorem Set.EAnnulus.oc_union_oo {X : Type u_1} [PseudoMetricSpace X] {x : X} {r r' R : ENNReal} (h₁ : r ≤ r') (h₂ : r' < R) : oc x r r' ∪ oo x r' R = oo x r R

@[simp]

theorem Set.EAnnulus.oc_union_oc {X : Type u_1} [PseudoMetricSpace X] {x : X} {r r' R : ENNReal} (h₁ : r ≤ r') (h₂ : r' ≤ R) : oc x r r' ∪ oc x r' R = oc x r R

@[simp]

theorem Set.EAnnulus.oo_union_co {X : Type u_1} [PseudoMetricSpace X] {x : X} {r r' R : ENNReal} (h₁ : r < r') (h₂ : r' ≤ R) : oo x r r' ∪ co x r' R = oo x r R

@[simp]

theorem Set.EAnnulus.oo_union_cc {X : Type u_1} [PseudoMetricSpace X] {x : X} {r r' R : ENNReal} (h₁ : r < r') (h₂ : r' ≤ R) : oo x r r' ∪ cc x r' R = oc x r R

@[simp]

theorem Set.EAnnulus.cc_union_oo {X : Type u_1} [PseudoMetricSpace X] {x : X} {r r' R : ENNReal} (h₁ : r ≤ r') (h₂ : r' < R) : cc x r r' ∪ oo x r' R = co x r R

@[simp]

theorem Set.EAnnulus.cc_union_oc {X : Type u_1} [PseudoMetricSpace X] {x : X} {r r' R : ENNReal} (h₁ : r ≤ r') (h₂ : r' ≤ R) : cc x r r' ∪ oc x r' R = cc x r R

@[simp]

theorem Set.EAnnulus.co_union_co {X : Type u_1} [PseudoMetricSpace X] {x : X} {r r' R : ENNReal} (h₁ : r ≤ r') (h₂ : r' ≤ R) : co x r r' ∪ co x r' R = co x r R

@[simp]

theorem Set.EAnnulus.co_union_cc {X : Type u_1} [PseudoMetricSpace X] {x : X} {r r' R : ENNReal} (h₁ : r ≤ r') (h₂ : r' ≤ R) : co x r r' ∪ cc x r' R = cc x r R

@[simp]

theorem Set.EAnnulus.oc_union_oi {X : Type u_1} [PseudoMetricSpace X] {x : X} {r R : ENNReal} (h : r ≤ R) : oc x r R ∪ oi x R = oi x r

@[simp]

theorem Set.EAnnulus.oo_union_ci {X : Type u_1} [PseudoMetricSpace X] {x : X} {r R : ENNReal} (h : r < R) : oo x r R ∪ ci x R = oi x r

@[simp]

theorem Set.EAnnulus.cc_union_oi {X : Type u_1} [PseudoMetricSpace X] {x : X} {r R : ENNReal} (h : r ≤ R) : cc x r R ∪ oi x R = ci x r

@[simp]

theorem Set.EAnnulus.co_union_ci {X : Type u_1} [PseudoMetricSpace X] {x : X} {r R : ENNReal} (h : r ≤ R) : co x r R ∪ ci x R = ci x r

theorem Set.EAnnulus.measurableSet_oo {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] {x : X} {r R : ENNReal} : MeasurableSet (oo x r R)

theorem Set.EAnnulus.measurableSet_oc {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] {x : X} {r R : ENNReal} : MeasurableSet (oc x r R)

theorem Set.EAnnulus.measurableSet_co {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] {x : X} {r R : ENNReal} : MeasurableSet (co x r R)

theorem Set.EAnnulus.measurableSet_cc {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] {x : X} {r R : ENNReal} : MeasurableSet (cc x r R)

theorem Set.EAnnulus.measurableSet_oi {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] {x : X} {r : ENNReal} : MeasurableSet (oi x r)

theorem Set.EAnnulus.measurableSet_ci {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] {x : X} {r : ENNReal} : MeasurableSet (ci x r)