infsep_zero_iff_subsingleton — Mathlib

English

Let s be finite. Then s.infsep = 0 if and only if s is subsingleton.

Русский

Пусть s является конечным. Тогда s.infsep = 0 эквивалентно тому, что s — субодиночное множество.

LaTeX

$$$\text{Finite}(s) \Rightarrow (s.infsep = 0 \iff s.Subsingleton)$$$

Lean4

theorem infsep_zero_iff_subsingleton (hs : s.Finite) : s.infsep = 0 ↔ s.Subsingleton :=
  letI := hs.fintype
  infsep_zero_iff_subsingleton_of_finite

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