infsep_zero_iff_subsingleton — Mathlib

English

For any Finset s, (s:Set α).infsep = 0 iff (s:Set α).Subsingeleton.

Русский

Для любого Finset s: (s:Set α).infsep = 0 тогда и только тогда, когда (s:Set α).Subsingeleton.

LaTeX

$$$\forall s:\mathrm{Finset}\,\alpha, (s.toSet.infsep = 0) \iff (s.toSet.Subsingleton)$$$

Lean4

theorem _root_.Finset.infsep_zero_iff_subsingleton (s : Finset α) : (s : Set α).infsep = 0 ↔ (s : Set α).Subsingleton :=
  infsep_zero_iff_subsingleton_of_finite

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