toComposition_boundaries — Mathlib

English

The boundaries of the associated Composition match the original boundaries.

Русский

Грани в соответствующем разложении совпадают с исходными гранями.

LaTeX

$$$c.toComposition.boundaries = c.boundaries$$$

Lean4

@[simp]
theorem toComposition_boundaries (c : CompositionAsSet n) : c.toComposition.boundaries = c.boundaries :=
  by
  ext ⟨j, hj⟩
  simp [c.mem_boundaries_iff_exists_blocks_sum_take_eq, Composition.boundaries, c.card_boundaries_eq_succ_length,
    Composition.boundary, Composition.sizeUpTo, Fin.exists_iff]

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