ofComposition_surj — Mathlib

English

A multiset l of natural numbers with sum n yields a partition of n by discarding zeros; the parts are l.filter(x ≠ 0).

Русский

Мультимножество натуральных чисел l с суммой n задаёт разбиение n, получаемое путём удаления нулей: parts = l \\{0}.

LaTeX

$$$$ (n,l,hl) \\mapsto \\text{parts} = l.\\text{filter}(\\,\\cdot \\neq 0) \\\\text{and}\\; (\\text{parts})_{sum} = n. $$$$

Lean4

theorem ofComposition_surj {n : ℕ} : Function.Surjective (ofComposition n) :=
  by
  rintro ⟨b, hb₁, hb₂⟩
  induction b using Quotient.inductionOn with
  | _ b => ?_
  exact
    ⟨⟨b, hb₁, by simpa using hb₂⟩, Partition.ext rfl⟩
      -- The argument `n` is kept explicit here since it is useful in tactic mode proofs to generate the
      -- proof obligation `l.sum = n`.

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