not_subset_empty

Mathlib.Data.Set.Subsingleton

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

English

If s is nontrivial, then s is not contained in the empty set: s ⊄ ∅.

Русский

Если множество s не тривиально, то оно не является подмножеством пустого множества: s ⊄ ∅.

LaTeX

$$s.Nontrivial \Rightarrow \lnot (s \subseteq \emptyset)$$

Lean4

theorem not_subset_empty (hs : s.Nontrivial) : ¬s ⊆ ∅ :=
  hs.nonempty.not_subset_empty

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

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

Разделы

Аффилиация

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