compositionEquiv — Mathlib

English

There is a canonical equivalence between the set of all compositions of n and the corresponding composition-as-set object.

Русский

Существует каноническое биекция между множеством всех разложений числа n и соответствующим объектом-разложением-как-набор.

LaTeX

$$$\\mathrm{compositionEquiv}(n):\\mathrm{Composition}(n) \\simeq \\mathrm{CompositionAsSet}(n)$$$

Lean4

/-- Equivalence between `Composition n` and `CompositionAsSet n`. -/
def compositionEquiv (n : ℕ) : Composition n ≃ CompositionAsSet n
    where
  toFun c := c.toCompositionAsSet
  invFun c := c.toComposition
  left_inv
    c := by
    ext1
    exact c.toCompositionAsSet_blocks
  right_inv
    c := by
    ext1
    exact c.toComposition_boundaries

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