English
Each composition corresponds to a CompositionAsSet with the same boundaries.
Русский
Каждой композиции соответствует CompositionAsSet с теми же границами.
LaTeX
$$$\\text{toCompositionAsSet}(c) \\,=\\, \\text{CompositionAsSet}(n)\\;\\text{with boundaries } c.boundaries$$$
Lean4
/-- To `c : Composition n`, one can associate a `CompositionAsSet n` by registering the leftmost
point of each block, and adding a virtual point at the right of the last block. -/
def toCompositionAsSet : CompositionAsSet n
where
boundaries := c.boundaries
zero_mem := by
simp only [boundaries, Finset.mem_univ, Finset.mem_map]
exact ⟨0, And.intro True.intro rfl⟩
getLast_mem := by
simp only [boundaries, Finset.mem_univ, Finset.mem_map]
exact ⟨Fin.last c.length, And.intro True.intro c.boundary_last⟩
