parts_nonempty

Mathlib.Order.Partition.Finpartition

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

English

If a ≠ ⊥, then P.parts is Nonempty.

Русский

Если a ≠ ⊥, то P.parts непусто.

LaTeX

$$$P \text{.parts Nonempty} \;\text{when } a \neq \bot$$$

Lean4

theorem parts_nonempty (P : Finpartition a) (ha : a ≠ ⊥) : P.parts.Nonempty :=
  parts_nonempty_iff.2 ha

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

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

Разделы

Аффилиация

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