Theorems · Theorem · general topology

exists_lt_subset_ball

∀ {α : Type u_1} [inst : PseudoMetricSpace α] [ProperSpace α] {x : α} {r : ℝ} {s : Set α},
  IsClosed s → s ⊆ Metric.ball x r → ∃ r' < r, s ⊆ Metric.ball x r'

If a ball in a proper space includes a closed set s, then there exists a ball with the same center and a strictly smaller radius that includes s.

Defined in

Mathlib.Topology.MetricSpace.ProperSpace.Lemmas

Cited by

1 results in Mathlib

Foundations

Depth 156 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PseudoMetricSpaceProperSpace