Inclusions of finite-radius balls, spheres, and annuli into extended-radius balls

In a pseudometric space, open balls Metric.eball c R with extended radius R : ℝ≥0∞ unify finite-radius open balls (R = ENNReal.ofReal R₀) with the whole space (R = ⊤). This file records set inclusions of finite-radius closed balls, spheres, and closed concentric annuli Metric.closedBall c R' \ Metric.ball c r' into Metric.eball c R and open concentric annuli Metric.eball c R \ Metric.closedBall c r when ENNReal.ofReal R' < R.

theorem TauCeti.closedBall_subset_eball {α : Type u_1} [PseudoMetricSpace α] {c : α} {r : ℝ} {R : ENNReal} (h : ENNReal.ofReal r < R) : Metric.closedBall c r ⊆ Metric.eball c R

If ENNReal.ofReal r < R, the closed ball Metric.closedBall c r is contained in the open extended-radius ball Metric.eball c R.

theorem TauCeti.sphere_subset_eball {α : Type u_1} [PseudoMetricSpace α] {c : α} {r : ℝ} {R : ENNReal} (h : ENNReal.ofReal r < R) : Metric.sphere c r ⊆ Metric.eball c R

If ENNReal.ofReal r < R, the sphere Metric.sphere c r is contained in the open extended-radius ball Metric.eball c R.

theorem TauCeti.closedBall_sdiff_ball_subset_eball_sdiff_closedBall {α : Type u_1} [PseudoMetricSpace α] {c : α} {r r' R' : ℝ} {R : ENNReal} (hrr' : r < r') (hR'R : ENNReal.ofReal R' < R) : Metric.closedBall c R' \ Metric.ball c r' ⊆ Metric.eball c R \ Metric.closedBall c r

If r < r' and ENNReal.ofReal R' < R, the closed concentric annulus Metric.closedBall c R' \ Metric.ball c r' is contained in the open concentric annulus Metric.eball c R \ Metric.closedBall c r.

theorem TauCeti.sphere_subset_eball_sdiff_closedBall {α : Type u_1} [PseudoMetricSpace α] {c : α} {r ρ : ℝ} {R : ENNReal} (hrρ : r < ρ) (hρR : ENNReal.ofReal ρ < R) : Metric.sphere c ρ ⊆ Metric.eball c R \ Metric.closedBall c r

Any sphere of radius ρ with r < ρ and ENNReal.ofReal ρ < R lies inside the open concentric annulus Metric.eball c R \ Metric.closedBall c r.