Theorems · Theorem · general topology

Metric.isSeparated_insert

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

Defined in

Mathlib.Topology.MetricSpace.MetricSeparated

Cited by

1 results in Mathlib

Foundations

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

Assumes

PseudoEMetricSpace