eq_singleton_iff_unique_mem — Mathlib

English

A set s equals {a} iff a ∈ s and every x ∈ s satisfies x = a.

Русский

Множество s равно {a} тогда и только тогда, когда a ∈ s и каждый x ∈ s выполняется x = a.

LaTeX

$$$s = \\{ a \\} \\iff a \\in s \\land \\forall x \\in s, x = a$$$

Lean4

theorem eq_singleton_iff_unique_mem : s = { a } ↔ a ∈ s ∧ ∀ x ∈ s, x = a :=
  Subset.antisymm_iff.trans <| and_comm.trans <| and_congr_left' singleton_subset_iff

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