support_single_add — Mathlib

English

For a Unique index type ι, the two representations AddEquiv.finsuppUnique and Equiv.finsuppUnique coincide on v.

Русский

При уникальном индексе ι две представления AddEquiv.finsuppUnique и Equiv.finsuppUnique совпадают на v.

LaTeX

$$$AddEquiv.finsuppUnique \\; v = Equiv.finsuppUnique \\; v$$$

Lean4

theorem support_single_add {a : ι} {b : M} {f : ι →₀ M} (ha : a ∉ f.support) (hb : b ≠ 0) :
    support (single a b + f) = cons a f.support ha := by
  classical
  have H := support_single_ne_zero a hb
  rw [support_add_eq, H, cons_eq_insert, insert_eq]
  rwa [H, disjoint_singleton_left]

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