nontrivial_iff_ne_singleton

Mathlib.Data.Set.Subsingleton

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

← MathLib Explorer

English

For ha: a ∈ s, s.Nontrivial iff s ≠ {a}.

Русский

Пусть ha: a ∈ s. Тогда s.Nontrivial эквивалентно s ≠ {a}.

LaTeX

$$(ha ∈ s) → (s.Nontrivial ↔ s ≠ {a})$$

Lean4

theorem nontrivial_iff_ne_singleton (ha : a ∈ s) : s.Nontrivial ↔ s ≠ { a } :=
  ⟨Nontrivial.ne_singleton, (eq_singleton_or_nontrivial ha).resolve_left⟩

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

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

Разделы

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

Аффилиация

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