English
If s is IsSeparated with parameter ε and every y ∈ s is at distance greater than ε from a new point x, then inserting x into s preserves separation: IsSeparated ε (insert x s).
Русский
Если s является ε-разделённым и каждый y ∈ s удовлетворяет edist(x,y) > ε, то добавление x к s сохраняет разделённость: IsSeparated ε (insert x s).
LaTeX
$$$\\text{IsSeparated}(\\varepsilon, s) \\to (\\forall y\\in s,\\ x\\neq y \\to \\varepsilon < \\operatorname{edist}(x,y)) \\Rightarrow \\text{IsSeparated}(\\varepsilon, \\operatorname{insert}(x,s)).$$$
Lean4
/-- A set `s` is `ε`-separated if its elements are pairwise at distance at least `ε` from each
other. -/
def IsSeparated (ε : ℝ≥0∞) (s : Set X) : Prop :=
s.Pairwise (ε < edist · ·)
