eq_empty_or_singleton — Mathlib

English

A subsingleton set is either empty or a singleton.

Русский

Любое субоднозначное множество либо пусто, либо состоит из одного элемента.

LaTeX

$$$ (s.Subsingleton) \Rightarrow (s = \emptyset \lor \exists x, s = \{ x \}) $$$

Lean4

theorem eq_empty_or_singleton (hs : s.Subsingleton) : s = ∅ ∨ ∃ x, s = { x } :=
  s.eq_empty_or_nonempty.elim Or.inl fun ⟨x, hx⟩ => Or.inr ⟨x, hs.eq_singleton_of_mem hx⟩

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