nonempty_of_mem_parts

Mathlib.Order.Partition.Finpartition

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

English

Every part of a Finpartition that lies in P.parts is nonempty.

Русский

Каждая часть разбиения Finpartition, принадлежащая P.parts, непустая.

LaTeX

$$$ a \in P.parts \Rightarrow a \neq \varnothing $$$

Lean4

theorem nonempty_of_mem_parts {a : Finset α} (ha : a ∈ P.parts) : a.Nonempty :=
  nonempty_iff_ne_empty.2 <| P.ne_bot ha

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

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

Разделы

Аффилиация

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