eq_singleton_or_nontrivial

Mathlib.Data.Set.Subsingleton

URI: https://scilib.ai/kg/mathlib#Set.eq_singleton_or_nontrivial

← MathLib Explorer

English

If a ∈ s, then s = {a} or s is nontrivial.

Русский

Пусть a ∈ s. Тогда s = {a} или s не тривиально.

LaTeX

$$(a ∈ s) → (s = {a} ∨ s.Nontrivial)$$

Lean4

theorem eq_singleton_or_nontrivial (ha : a ∈ s) : s = { a } ∨ s.Nontrivial := by rw [← subsingleton_iff_singleton ha];
  exact s.subsingleton_or_nontrivial

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

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

Разделы

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

Аффилиация

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