exists_eq_singleton_or_nontrivial

Mathlib.Data.Set.Subsingleton

URI: https://scilib.ai/kg/mathlib#Set.Nonempty.exists_eq_singleton_or_nontrivial

← MathLib Explorer

English

With a Nontrivial α, the singleton {a} is a strict subset of univ.

Русский

При неtrивиальном α множество {a} является строгим подмножеством univ.

LaTeX

$$[Nontrivial α] ( {a} ⊂ univ )$$

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

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru