ne_empty

Mathlib.Order.Partition.Finpartition

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

English

If t ∈ P.parts, then t ≠ ∅.

Русский

Если t ∈ P.parts, то t ≠ ∅.

LaTeX

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

Lean4

theorem ne_empty (h : t ∈ P.parts) : t ≠ ∅ :=
  P.ne_bot h

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

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

Разделы

Аффилиация

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