not_subset_singleton

Mathlib.Data.Set.Subsingleton

URI: https://scilib.ai/kg/mathlib#Set.Nontrivial.not_subset_singleton

← MathLib Explorer

English

If s is nontrivial, then s is not contained in any singleton: ¬(s ⊆ {x}).

Русский

Если множество s не тривиально, то оно не подмножество множества {x} для любого x.

LaTeX

$$∀ {x}, s.Nontrivial → ¬(s ⊆ {x})$$

Lean4

theorem not_subset_singleton {x} (hs : s.Nontrivial) : ¬s ⊆ { x } :=
  (not_congr subset_singleton_iff_eq).2 (not_or_intro hs.ne_empty hs.ne_singleton)

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

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

Разделы

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

Аффилиация

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