coe_infsep_of_offDiag_nonempty — Mathlib

English

If s is a finite set with offDiag nonempty, then s.infsep equals the minimum of distances over the offDiag pairs, i.e., the minimal distance between two distinct elements of s.

Русский

Если s — конечное множество с непустой offDiag, то s.infsep равна минимальному расстоянию между двумя различными элементами множества.

LaTeX

$$$\displaystyle (s:\mathrm{Set}\alpha).infsep = (s.offDiag).inf' (hs) (\operatorname{uncurry dist})$, где hs: s.offDiag.Nonempty.$$

Lean4

theorem _root_.Finset.coe_infsep_of_offDiag_nonempty [DecidableEq α] {s : Finset α} (hs : s.offDiag.Nonempty) :
    (s : Set α).infsep = s.offDiag.inf' hs (uncurry dist) := by rw [Finset.coe_infsep, dif_pos hs]

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