reverse — Mathlib

English

Reverse the order of blocks in a composition; the blocks are reversed and the total sum remains the same (up to index reindexing).

Русский

Порядок блоков композиции меняется на обратный; сумма блоков сохраняется.

LaTeX

$$$\\mathrm{reverse}(c)\\;: \\mathrm{Composition}(n)\\to \\mathrm{Composition}(n),\\ \\mathrm{blocks}=[c.\\mathrm{blocks}]^\\mathrm{reverse},\\ \\mathrm{blocks\\_sum}=c.\\mathrm{blocks\\_sum}.$$$

Lean4

/-- Reverse the order of blocks in a composition. -/
@[simps]
def reverse (c : Composition n) : Composition n
    where
  blocks := c.blocks.reverse
  blocks_pos hi := c.blocks_pos (mem_reverse.mp hi)
  blocks_sum := by simp [List.sum_reverse]

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