English
For a nontrivial s, infsep(s) equals the iInf over offDiag of dist.
Русский
Для нетривиального s инфsep(s) равен iInf расстояний между парами точек.
LaTeX
$$$ s.Nontrivial \rightarrow s.infsep = \inf_{d \in s.offDiag} (uncurry dist) (d : α \times α) $$$
Lean4
theorem infsep_eq_iInf [Decidable s.Nontrivial] :
s.infsep = if s.Nontrivial then ⨅ d : s.offDiag, (uncurry dist) (d : α × α) else 0 :=
by
split_ifs with hs
· have hb : BddBelow (uncurry dist '' s.offDiag) :=
by
refine ⟨0, fun d h => ?_⟩
simp_rw [mem_image, Prod.exists, uncurry_apply_pair] at h
rcases h with ⟨_, _, _, rfl⟩
exact dist_nonneg
refine eq_of_forall_le_iff fun _ => ?_
simp_rw [hs.le_infsep_iff, le_ciInf_set_iff (offDiag_nonempty.mpr hs) hb, imp_forall_iff, mem_offDiag, Prod.forall,
uncurry_apply_pair, and_imp]
· exact (not_nontrivial_iff.mp hs).infsep_zero
