nontrivial_iff_ne_singleton

Mathlib.Data.Finset.Insert

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

← MathLib Explorer

English

For a ∈ s, s.Nontrivial is equivalent to s ≠ {a}.

Русский

Для a ∈ s, непустость равнозначна неравенству s и {a}.

LaTeX

$$s.Nontrivial \iff s \neq \{ 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