Theorems · Theorem · general topology

Set.einfsep_pos

∀ {α : Type u_1} [inst : EDist α] {s : Set α}, 0 < s.einfsep ↔ ∃ C > 0, ∀ x ∈ s, ∀ y ∈ s, x ≠ y → C ≤ edist x y

Defined in

Mathlib.Topology.MetricSpace.Infsep

Cited by

1 results in Mathlib

Foundations

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

Assumes

EDist