parts_nonempty_iff

Mathlib.Order.Partition.Finpartition

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

English

P.parts.Nonempty is equivalent to a ≠ ⊥.

Русский

Непустота частей P равна не равенству a ⊥.

LaTeX

$$$P.parts.Nonempty \iff a \neq \bot$$$

Lean4

@[simp]
theorem parts_nonempty_iff : P.parts.Nonempty ↔ a ≠ ⊥ := by rw [nonempty_iff_ne_empty, not_iff_not, parts_eq_empty_iff]

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

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

Разделы

Аффилиация

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