infsep_eq_iInf — Mathlib

English

If s.Nontrivial, infsep(s) equals iInf over offDiag of distances.

Русский

Если s не тривиально, то инфsep(s) равно iInf расстояний между неравными парами точек.

LaTeX

$$$ {s.Nontrivial} \rightarrow s.infsep = iInf (fun d => dist d.1 d.2) $$$

Lean4

theorem infsep_eq_iInf (hs : s.Nontrivial) : s.infsep = ⨅ d : s.offDiag, (uncurry dist) (d : α × α) := by
  classical rw [Set.infsep_eq_iInf, if_pos hs]

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