partition_one_parts — Mathlib

English

If p is a partition of 1, then p.parts = {1}.

Русский

Если p — разбиение числа 1, то p.parts = {1}.

LaTeX

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

Lean4

@[simp]
theorem partition_one_parts (p : Partition 1) : p.parts = { 1 } :=
  by
  have h : p.parts = replicate (card p.parts) 1 :=
    eq_replicate_card.2 fun x hx => ((le_sum_of_mem hx).trans_eq p.parts_sum).antisymm (p.parts_pos hx)
  have h' : card p.parts = 1 := by simpa using (congrArg sum h.symm).trans p.parts_sum
  rw [h, h', replicate_one]

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