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 Ico, as they would be balls.

We also define EAnnulus similarly using edist instead of dist.

Tags

annulus, eannulus

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₂

@[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.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)

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 : r ≥ 0) : 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 : r ≥ 0) : 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 : r > 0 ∨ R ≥ 0) : 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 : r ≥ 0) : 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)