exists_eq_singleton_or_nontrivial

English

Let s be a finite nonempty set. Then either s is a singleton {a} for some a, or s is nontrivial (contains at least two elements).

Русский

Пусть s — конечное непустое множество. Тогда либо оно равно множеству {a} для некоторого a, либо оно не тривиально (содержит как минимум два элемента).

LaTeX

$$$s \neq \emptyset \Rightarrow (\exists a, s = \{a\}) \lor (s.card > 1)$$$

Lean4

theorem exists_eq_singleton_or_nontrivial : s.Nonempty → (∃ a, s = { a }) ∨ s.Nontrivial := fun ⟨a, ha⟩ =>
  (eq_singleton_or_nontrivial ha).imp_left <| Exists.intro a

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