boundaries — Mathlib

English

The set of boundaries is the image of all indices under the boundary map.

Русский

Множество границ является образом множества индексов под отображение границ.

LaTeX

$$$\\text{boundaries}(c) = \\{ \\text{boundary}(i) : i \\in \\{0,1,...,c.length\\} \\}$$$

Lean4

/-- The boundaries of a composition, i.e., the leftmost point of all the blocks. We include
a virtual point at the right of the last block, to make for a nice equiv with
`CompositionAsSet n`. -/
def boundaries : Finset (Fin (n + 1)) :=
  Finset.univ.map c.boundary.toEmbedding

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