accumulate_last — Mathlib

English

If n ≤ m, the map accumulate n m is injective on Fin n → ℕ with codomain Fin m → ℕ.

Русский

При n ≤ m отображение accumulate n m инъективно на пространстве функций Fin n → ℕ в Fin m → ℕ.

LaTeX

$$$\\text{If } n \\le m,\\quad \\mathrm{accumulate}_{n,m} \\text{ is injective}$$$

Lean4

theorem accumulate_last {i n m : ℕ} (hin : i < n) (hmi : m = i + 1) (t : Fin n → ℕ)
    (ht : ∀ j : Fin n, m ≤ j → t j = 0) : accumulate n m t ⟨i, i.lt_succ_self.trans_eq hmi.symm⟩ = t ⟨i, hin⟩ :=
  by
  rw [accumulate_apply]
  apply sum_eq_single_of_mem
  · rw [mem_filter]; exact ⟨mem_univ _, le_rfl⟩
  refine fun j hij hji ↦ ht j ?_
  rw [mem_filter_univ] at hij
  exact hmi.trans_le (hij.lt_of_ne (Fin.val_ne_iff.2 hji).symm).nat_succ_le

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