empty_notMem_parts

Mathlib.Order.Partition.Finpartition

URI: https://scilib.ai/kg/mathlib#Finpartition.empty_notMem_parts

English

The empty set is not a member of the parts of a Finpartition.

Русский

Пустое множество не является частью разбиения Finpartition.

LaTeX

$$$ \emptyset \notin P.parts $$$

Lean4

@[simp]
theorem empty_notMem_parts : ∅ ∉ P.parts :=
  P.bot_notMem

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

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

Разделы

Аффилиация

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