English
If s is finite and decidable nontrivial, then infsep can be computed as a finite inf' over offDiag.
Русский
Если s конечное множество и допускается решение, то infsep
можно вычислить как конечный inf' по парам элементов.
LaTeX
$$$ [Decidable s.Nontrivial] [DecidableEq \alpha] [Fintype s] : s.infsep = if hs : s.Nontrivial then s.offDiag.toFinset.inf' (by simpa) (uncurry dist) else 0 $$$
Lean4
theorem infsep_of_fintype [Decidable s.Nontrivial] [DecidableEq α] [Fintype s] :
s.infsep = if hs : s.Nontrivial then s.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, mem_toFinset, mem_offDiag, Prod.forall,
uncurry_apply_pair, and_imp]
· rw [not_nontrivial_iff] at hs
exact hs.infsep_zero
