Theorems · Theorem · general topology

eventually_closedBall_subset

∀ {α : Type u_2} [inst : PseudoMetricSpace α] {x : α} {u : Set α},
  u ∈ nhds x → ∀ᶠ (r : ℝ) in nhds 0, Metric.closedBall x r ⊆ u

If u is a neighborhood of x, then for small enough r, the closed ball Metric.closedBall x r is contained in u.

Defined in

Mathlib.Topology.MetricSpace.Pseudo.Lemmas

Cited by

3 results in Mathlib

Foundations

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

Assumes

PseudoMetricSpace