isSeparated_insert_of_notMem — Mathlib

English

If x ∉ s, then IsSeparated ε (insert x s) holds iff IsSeparated ε s and ∀ y ∈ s, ε < edist(x,y).

Русский

Если x не в s, то ε-разделённость множества insert(x,s) равносильна ε-разделённости s и неравенству ε < edist(x,y) для всех y ∈ s.

LaTeX

$$$(x \\notin s) \\Rightarrow \\big( \\operatorname{AreSeparated}(\\varepsilon, \\operatorname{insert}(x,s)) \\iff \\operatorname{AreSeparated}(\\varepsilon, s) \\land \\forall y \\in s, \\varepsilon < \\operatorname{edist}(x,y) \\big).$$$

Lean4

theorem isSeparated_insert_of_notMem (hx : x ∉ s) :
    IsSeparated ε (insert x s) ↔ IsSeparated ε s ∧ ∀ y ∈ s, ε < edist x y :=
  pairwise_insert_of_symmetric_of_notMem (fun _ _ ↦ by simp [edist_comm]) hx

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