English
The blocks of the associated CompositionAsSet coincide with the original blocks.
Русский
Блоки в составе-как-набор совпадают с исходными блоками.
LaTeX
$$$\\mathrm{toCompositionAsSet}.blocks = c.blocks$$$
Lean4
@[simp]
theorem toCompositionAsSet_blocks (c : Composition n) : c.toCompositionAsSet.blocks = c.blocks :=
by
let d := c.toCompositionAsSet
change d.blocks = c.blocks
have length_eq : d.blocks.length = c.blocks.length := by simp [d, blocks_length]
suffices H : ∀ i ≤ d.blocks.length, (d.blocks.take i).sum = (c.blocks.take i).sum from eq_of_sum_take_eq length_eq H
intro i hi
have i_lt : i < d.boundaries.card := by
simpa [CompositionAsSet.blocks, length_ofFn, d.card_boundaries_eq_succ_length] using Nat.lt_succ_iff.2 hi
have i_lt' : i < c.boundaries.card := i_lt
have i_lt'' : i < c.length + 1 := by rwa [c.card_boundaries_eq_succ_length] at i_lt'
have A :
d.boundaries.orderEmbOfFin rfl ⟨i, i_lt⟩ =
c.boundaries.orderEmbOfFin c.card_boundaries_eq_succ_length ⟨i, i_lt''⟩ :=
rfl
have B : c.sizeUpTo i = c.boundary ⟨i, i_lt''⟩ := rfl
rw [d.blocks_partial_sum i_lt, CompositionAsSet.boundary, ← Composition.sizeUpTo, B, A, c.orderEmbOfFin_boundaries]
