partition_zero_parts — Mathlib

English

The unique partition of 0 has empty parts, i.e., p.parts = 0 for every p : Partition 0.

Русский

Единственное разбиение числа 0 имеет пустые части, то есть для любого p : Partition 0 выполняется p.parts = 0.

LaTeX

$$$\forall p \in \mathrm{Partition}(0),\ p.\mathrm{parts} = 0$$$

Lean4

@[simp]
theorem partition_zero_parts (p : Partition 0) : p.parts = 0 :=
  eq_zero_of_forall_notMem fun _ h => (p.parts_pos h).ne' <| sum_eq_zero_iff.1 p.parts_sum _ h

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