insert — Mathlib

English

If s is ε-separated and every y ∈ s satisfies x ≠ y → ε < edist x y, then insert x s is ε-separated.

Русский

Если s ε-разделено и для каждого y ∈ s выполнено x ≠ y → ε < edist x y, то insert x s ε-разделено.

LaTeX

$$$\\operatorname{AreSeparated}(\\varepsilon, s) \\to (\\forall y \\in s, x \\neq y \\to \\varepsilon < \\operatorname{edist}(x,y)) \\Rightarrow \\operatorname{AreSeparated}(\\varepsilon, \\operatorname{insert}(x,s)).$$$

Lean4

protected theorem insert (hs : IsSeparated ε s) (h : ∀ y ∈ s, x ≠ y → ε < edist x y) : IsSeparated ε (insert x s) :=
  isSeparated_insert.2 ⟨hs, h⟩

Похожие утверждения