ne_single_iff — Mathlib

English

For a composition c of n with n>0, c is not the single n-block composition iff every block size is strictly less than n.

Русский

Для композиции c размера n (>0) утверждается: c ≠ single n h тогда и только тогда, когда все размеры блоков строго меньше n.

LaTeX

$$$c \\neq \\mathrm{single}\\;n\\;h \\ \\iff\\ \\forall i\\in\\mathrm{Fin}(c.\\mathrm{length}),\\ c.\\mathrm{blocksFun}(i) < n.$$$

Lean4

theorem ne_single_iff {n : ℕ} (hn : 0 < n) {c : Composition n} : c ≠ single n hn ↔ ∀ i, c.blocksFun i < n :=
  by
  rw [← not_iff_not]
  push_neg
  constructor
  · rintro rfl
    exact ⟨⟨0, by simp⟩, by simp⟩
  · rintro ⟨i, hi⟩
    rw [eq_single_iff_length]
    have : ∀ j : Fin c.length, j = i := by
      intro j
      by_contra ji
      apply lt_irrefl (∑ k, c.blocksFun k)
      calc
        ∑ k, c.blocksFun k ≤ c.blocksFun i := by simp only [c.sum_blocksFun, hi]
        _ < ∑ k, c.blocksFun k :=
          Finset.single_lt_sum ji (Finset.mem_univ _) (Finset.mem_univ _) (c.one_le_blocksFun j) fun _ _ _ => zero_le _
    simpa using Fintype.card_eq_one_of_forall_eq this

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