sigma_eq_iff_blocks_eq — Mathlib

English

Two pairs (n, c) and (n', c') are equal if and only if their second components have equal blocks: c = c' ⇔ c.2.blocks = c'.2.blocks.

Русский

Две пары (n, c) и (n', c') равны тогда и только тогда, когда их вторые компоненты имеют одинаковые блоки: c = c' ⇔ c.2.blocks = c'.2.blocks.

LaTeX

$$$ c = c' \\iff c.2.blocks = c'.2.blocks $$$

Lean4

/-- Two compositions (possibly of different integers) coincide if and only if they have the
same sequence of blocks. -/
theorem sigma_eq_iff_blocks_eq {c : Σ n, Composition n} {c' : Σ n, Composition n} : c = c' ↔ c.2.blocks = c'.2.blocks :=
  by
  refine ⟨fun H => by rw [H], fun H => ?_⟩
  rcases c with ⟨n, c⟩
  rcases c' with ⟨n', c'⟩
  have : n = n' := by rw [← c.blocks_sum, ← c'.blocks_sum, H]
  induction this
  congr
  ext1
  exact H

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