einfsep — Mathlib

English

For a finite set s, einfsep(s) is the infimum over all unordered/distinct pairs in s of the distance edist.

Русский

Для конечного множества s einfsep есть как инфимума расстояний по всем различным парам точек из s.

LaTeX

$$$ \operatorname{einfsep}(s) = \inf_{(x,y) \in s\times s,\; x \neq y} \operatorname{edist}(x,y) $$$

Lean4

theorem einfsep (hs : s.Finite) : s.einfsep = hs.offDiag.toFinset.inf (uncurry edist) :=
  by
  refine eq_of_forall_le_iff fun _ => ?_
  simp_rw [le_einfsep_iff, imp_forall_iff, Finset.le_inf_iff, Finite.mem_toFinset, mem_offDiag, Prod.forall,
    uncurry_apply_pair, and_imp]

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