nonempty_iff_eq_singleton_default

English

There exists exactly one element in s if and only if s is a singleton.

Русский

Существует ровно один элемент в s тогда и только тогда, когда s является синглтоном.

LaTeX

$$$\exists a, s = \{ a \} \iff \exists! a, a \in s$$$

Lean4

theorem nonempty_iff_eq_singleton_default [Unique α] {s : Finset α} : s.Nonempty ↔ s = { default } := by
  simp [eq_singleton_iff_nonempty_unique_mem, eq_iff_true_of_subsingleton]

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