instDecidableEqPartition — Mathlib

English

For every partition μ of n there exists a composition c of n with ofComposition n c = μ; the map ofComposition is surjective.

Русский

Для любого разбиения μ числа n существует композиция c числа n такая, что ofComposition n c = μ; отображение на композиции сюръектно.

LaTeX

$$$ \exists c,\; f(c) = μ \quad\text{where } f = \mathrm{Nat.Partition.ofComposition}\, n$$$

Lean4

instance instDecidableEqPartition {n✝} : DecidableEq✝ (@Nat.Partition✝ n✝) :=
  instDecidableEqPartition.decEq

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