einfsep_insert_le — Mathlib

English

If you insert a point x into a set s, the Einfsep of the new set is at most the distance from x to the closest point of s (excluding x itself to avoid the trivial pair).

Русский

При добавлении точки x в множество s новой точке x сопоставляется расстояние до ближайшей точки из s (если y ≠ x); einfsep(insert x s) не больше этого расстояния.

LaTeX

$$$ \operatorname{einfsep}(\{x\} \cup s) \le \inf_{y \in s,\ y \neq x} \operatorname{edist}(x,y) $$$

Lean4

theorem einfsep_insert_le : (insert x s).einfsep ≤ ⨅ (y ∈ s) (_ : x ≠ y), edist x y :=
  by
  simp_rw [le_iInf_iff]
  exact fun _ hy hxy => einfsep_le_edist_of_mem (mem_insert _ _) (mem_insert_of_mem _ hy) hxy

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