not_ssubset_empty

Mathlib.Data.Finset.Empty

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

English

No Finset is a strict subset of the empty set.

Русский

Никакое множество не является строгим подмножеством пустого множества.

LaTeX

$$$\\\\forall s: Finset\\\\, s \\\\nsubset \\\\emptyset \\\\Rightarrow False$$$

Lean4

@[simp]
theorem not_ssubset_empty (s : Finset α) : ¬s ⊂ ∅ := by grind

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

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

Разделы

Аффилиация

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