exists_eq_singleton_iff_nonempty_subsingleton

English

A set s is a singleton if and only if it is nonempty and subsingleton.

Русский

Множество s является единичным тогда и только тогда, когда оно непусто и подсинглотонно.

LaTeX

$$$ (\exists a : \alpha, s = \{a\}) \iff (s.Nonempty \wedge s.Subsingleton) $$$

Lean4

theorem exists_eq_singleton_iff_nonempty_subsingleton : (∃ a : α, s = { a }) ↔ s.Nonempty ∧ s.Subsingleton :=
  by
  refine ⟨?_, fun h => ?_⟩
  · rintro ⟨a, rfl⟩
    exact ⟨singleton_nonempty a, subsingleton_singleton⟩
  · exact h.2.eq_empty_or_singleton.resolve_left h.1.ne_empty

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