English
c = ones n iff c.length = n.
Русский
c = ones n тогда и только тогда, когда c.length = n.
LaTeX
$$$ c = \\text{ones}(n) \\iff c.length = n $$$
Lean4
theorem eq_ones_iff_length {c : Composition n} : c = ones n ↔ c.length = n :=
by
constructor
· rintro rfl
exact ones_length n
· contrapose
intro H length_n
apply lt_irrefl n
calc
n = ∑ i : Fin c.length, 1 := by simp [length_n]
_ < ∑ i : Fin c.length, c.blocksFun i := by
{
obtain ⟨i, hi, i_blocks⟩ : ∃ i ∈ c.blocks, 1 < i := ne_ones_iff.1 H
rw [← ofFn_blocksFun, mem_ofFn' c.blocksFun, Set.mem_range] at hi
obtain ⟨j : Fin c.length, hj : c.blocksFun j = i⟩ := hi
rw [← hj] at i_blocks
exact Finset.sum_lt_sum (fun i _ => one_le_blocksFun c i) ⟨j, Finset.mem_univ _, i_blocks⟩
}
_ = n := c.sum_blocksFun