English
If a is not in the support of f and b ≠ 0, then supp(f + single a b) = cons a f.support ha, i.e., the support is the union of a with the support of f, with a counted once.
Русский
Если a не принадлежит поддержке f и b ≠ 0, то supp(f + single a b) = cons a f.support ha, т.е. поддержка равна объединению {a} с поддержкой f.
LaTeX
$$$\\operatorname{supp}(f + \\mathrm{single}_a(b)) = \\operatorname{cons}(a, \\operatorname{supp}(f))_{ha}$$$
Lean4
theorem support_add_single {a : ι} {b : M} {f : ι →₀ M} (ha : a ∉ f.support) (hb : b ≠ 0) :
support (f + single a b) = cons a f.support ha := by
classical
have H := support_single_ne_zero a hb
rw [support_add_eq, H, union_comm, cons_eq_insert, insert_eq]
rwa [H, disjoint_singleton_right]
