eq_ones_iff_length — Mathlib

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

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