English
c = ones n iff for all i, i ∈ blocks implies i = 1.
Русский
c = ones n тогда и только тогда, когда каждый элемент блока равен 1.
LaTeX
$$$ c = \\text{ones}(n) \\iff \\forall i \\in c.blocks, i = 1 $$$
Lean4
theorem eq_ones_iff {c : Composition n} : c = ones n ↔ ∀ i ∈ c.blocks, i = 1 :=
by
constructor
· rintro rfl
exact fun i => eq_of_mem_replicate
· intro H
ext1
have A : c.blocks = replicate c.blocks.length 1 := eq_replicate_of_mem H
have : c.blocks.length = n := by
conv_rhs => rw [← c.blocks_sum, A]
simp
rw [A, this, ones_blocks]