singleton_iff_unique_mem — Mathlib

English

A Finset s has the form s = {a} exactly when there exists a unique a with a ∈ s.

Русский

Финсет s имеет вид s = {a} тогда и только тогда, когда существует единственный элемент a, удовлетворяющий a ∈ s.

LaTeX

$$$\text{Singleton exists uniquely: } \exists a, s = \{ a \} \iff \exists! a, a \in s$$$

Lean4

theorem singleton_iff_unique_mem (s : Finset α) : (∃ a, s = { a }) ↔ ∃! a, a ∈ s := by
  simp only [eq_singleton_iff_unique_mem, ExistsUnique]

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