English
Let (α, d) be a pseudo-metric space and s ⊆ α be finite. Then s.infsep equals 0 if s has at most one point; otherwise it equals the minimum distance between two distinct points of s. Equivalently, s.infsep = min{ dist(x,y) : x,y ∈ s, x ≠ y } when s.Nontrivial, and 0 when s is trivial.
Русский
Пусть (α, d) — псевдометрическое пространство и s ⊆ α конечно. Тогда s.infsep равно 0, если в s не более одной точки; иначе это минимальное расстояние между двумя различными точками множества s. Эквивалентно: s.infsep = min{ dist(x,y) : x,y ∈ s, x ≠ y } при s.Nontrivial, и 0 в противном случае.
LaTeX
$$$\displaystyle s\text{ infsep } = \begin{cases}0, & \neg s.Nontrivial, \\ \min_{x \in s,\ y \in s,\ x \neq y} \operatorname{dist}(x,y), & s.Nontrivial.\end{cases}$$$
Lean4
theorem infsep [Decidable s.Nontrivial] (hsf : s.Finite) :
s.infsep = if hs : s.Nontrivial then hsf.offDiag.toFinset.inf' (by simpa) (uncurry dist) else 0 :=
by
split_ifs with hs
· refine eq_of_forall_le_iff fun _ => ?_
simp_rw [hs.le_infsep_iff, imp_forall_iff, Finset.le_inf'_iff, Finite.mem_toFinset, mem_offDiag, Prod.forall,
uncurry_apply_pair, and_imp]
· rw [not_nontrivial_iff] at hs
exact hs.infsep_zero
