toComposition — Mathlib

English

Associating a composition-as-set to a composition yields a standard composition with the same blocks.

Русский

Ассоциация разложения-как-набор к разложениям возвращает обычное разложение с теми же блоками.

LaTeX

$$$\\text{toComposition}(c)$ is the composition with blocks = $c.blocks$, and $\\text{blocks\_sum} = c.blocks\_sum$.$$

Lean4

/-- Associating a `Composition n` to a `CompositionAsSet n`, by registering the sizes of the
blocks as a list of positive integers. -/
def toComposition : Composition n where
  blocks := c.blocks
  blocks_pos := by simp only [blocks, forall_mem_ofFn_iff, blocksFun_pos c, forall_true_iff]
  blocks_sum := c.blocks_sum

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