einfsep_of_fintype — Mathlib

English

If s is finite, then the Einfsep equals the infimum of the distances over all distinct pairs of elements of s.

Русский

Если множество конечно, то einfsep равно инфимума расстояний по всем различным парам элементов множества.

LaTeX

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

Lean4

theorem einfsep_of_fintype [DecidableEq α] [Fintype s] : s.einfsep = s.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, mem_toFinset, mem_offDiag, Prod.forall,
    uncurry_apply_pair, and_imp]

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