Theorems · Theorem · general topology

Metric.IsSeparated.insert

∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {s : Set X} {ε : ENNReal} {x : X},
  Metric.IsSeparated ε s → (∀ y ∈ s, x ≠ y → ε < edist x y) → Metric.IsSeparated ε (insert x s)

Defined in

Mathlib.Topology.MetricSpace.MetricSeparated

Cited by

0 results in Mathlib

Foundations

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

Assumes

PseudoEMetricSpace