English
For a finite set expressed as a Finset s, the infsep of the corresponding Set is given by the same conditional formula as for sets: it is the off-diagonal minimum distance if the off-diagonal set is nonempty, otherwise 0.
Русский
Для конечного множества, записанного как Finset s, инфсеп соответствующего множества задаётся той же условной формулой: это минимальное расстояние по диагонали вне диагонали, если offDiag не пустое, иначе 0.
LaTeX
$$$\displaystyle (s:\!\mathrm{Set}\,\alpha).infsep = \begin{cases} (s.offDiag).inf' (hs) (\operatorname{uncurry dist}), & \text{если } s.offDiag \neq \emptyset, \\ 0, & \text{иначе.} \end{cases}$$$
Lean4
theorem _root_.Finset.coe_infsep [DecidableEq α] (s : Finset α) :
(s : Set α).infsep = if hs : s.offDiag.Nonempty then s.offDiag.inf' hs (uncurry dist) else 0 :=
by
have H : (s : Set α).Nontrivial ↔ s.offDiag.Nonempty := by
rw [← Set.offDiag_nonempty, ← Finset.coe_offDiag, Finset.coe_nonempty]
split_ifs with hs
· simp_rw [(H.mpr hs).infsep_of_fintype, ← Finset.coe_offDiag, Finset.toFinset_coe]
· exact (not_nontrivial_iff.mp (H.mp.mt hs)).infsep_zero
