coe_einfsep — Mathlib

English

For a finite set s represented as a Finset, the Einfsep equals the infimum of the distances over all unordered pairs from s.

Русский

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

LaTeX

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

Lean4

theorem coe_einfsep [DecidableEq α] {s : Finset α} : (s : Set α).einfsep = s.offDiag.inf (uncurry edist) := by
  simp_rw [einfsep_of_fintype, ← Finset.coe_offDiag, Finset.toFinset_coe]

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