infsep_zero_iff_subsingleton_of_finite

English

For a finite s, s.infsep = 0 if and only if s is subsingleton (has at most one point).

Русский

Для конечного s: s.infsep = 0 тогда и только тогда, когда s субодиночно (не более одной точки).

LaTeX

$$$\forall s:\mathrm{Set}(.).\infsep = 0 \iff s\text{ subsingleton}$$$

Lean4

theorem infsep_zero_iff_subsingleton_of_finite [Finite s] : s.infsep = 0 ↔ s.Subsingleton :=
  by
  rw [infsep_zero, einfsep_eq_top_iff, or_iff_right_iff_imp]
  exact fun H => (einfsep_pos_of_finite.ne' H).elim

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