eq_single_iff_length — Mathlib

English

For a composition c of n with n>0, c equals the single n-block composition iff c has length 1.

Русский

Для композиции c размера n с n>0 выполняется: c = single n h тогда и только тогда, когда длина c равна 1.

LaTeX

$$$c = \\mathrm{single}\\;n\\;h \\;\\Longleftrightarrow\\; \\mathrm{length}(c) = 1,$$$

Lean4

theorem eq_single_iff_length {n : ℕ} (h : 0 < n) {c : Composition n} : c = single n h ↔ c.length = 1 :=
  by
  constructor
  · intro H
    rw [H]
    exact single_length h
  · intro H
    ext1
    have A : c.blocks.length = 1 := H ▸ c.blocks_length
    have B : c.blocks.sum = n := c.blocks_sum
    rw [eq_cons_of_length_one A] at B ⊢
    simpa [single_blocks] using B

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