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: looks ready (once the dependent file is upstreamed); 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.iUnion_co_eq_ci {X : Type u_1} [PseudoMetricSpace X] {x : X} {f : ℕ → ℝ} (hf : ∀ (n : ℕ), f 0 ≤ f n) (h2f : ¬BddAbove (range f)) : ⋃ (i : ℕ), co x (f i) (f (i + 1)) = ci x (f 0)

theorem Set.Annulus.iUnion_oc_eq_oi {X : Type u_1} [PseudoMetricSpace X] {x : X} {f : ℕ → ℝ} (hf : ∀ (n : ℕ), f 0 ≤ f n) (h2f : ¬BddAbove (range f)) : ⋃ (i : ℕ), oc x (f i) (f (i + 1)) = oi x (f 0)

theorem Set.Annulus.pairwise_disjoint_co_monotone {X : Type u_1} [PseudoMetricSpace X] {ι : Type u_2} [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_oc_monotone {X : Type u_1} [PseudoMetricSpace X] {ι : Type u_2} [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)