English
If we insert x into s, then einfsep(insert x s) equals the minimum of the two contributions: the distances from x to s (excluding x itself) and the previous einfsep of s.
Русский
При добавлении x в s, einfsep(insert x s) равняется минимуму: расстояний от x до элементов s (исключая x) и предыдущего einfsep(s).
LaTeX
$$$ \operatorname{einfsep}(\{x\} \cup s) = \min\left( \inf_{y \in s,\ y \neq x} \operatorname{edist}(x,y), \operatorname{einfsep}(s) \right) $$$
Lean4
theorem einfsep_insert : einfsep (insert x s) = (⨅ (y ∈ s) (_ : x ≠ y), edist x y) ⊓ s.einfsep :=
by
refine le_antisymm (le_min einfsep_insert_le (einfsep_anti (subset_insert _ _))) ?_
simp_rw [le_einfsep_iff, inf_le_iff, mem_insert_iff]
rintro y (rfl | hy) z (rfl | hz) hyz
· exact False.elim (hyz rfl)
· exact Or.inl (iInf_le_of_le _ (iInf₂_le hz hyz))
· rw [edist_comm]
exact Or.inl (iInf_le_of_le _ (iInf₂_le hy hyz.symm))
· exact Or.inr (einfsep_le_edist_of_mem hy hz hyz)
