support_sub — Mathlib

English

For finitely supported f,g : ι →₀ G, the support of f - g is contained in the union of supports: supp(f - g) ⊆ supp(f) ∪ supp(g).

Русский

Для функций с конечной опорой f,g: supp(f - g) ⊆ supp(f) ∪ supp(g).

LaTeX

$$$\operatorname{support}(f - g) \subseteq \operatorname{support}(f) \cup \operatorname{support}(g).$$$

Lean4

theorem support_sub [DecidableEq ι] {f g : ι →₀ G} : support (f - g) ⊆ support f ∪ support g :=
  by
  rw [sub_eq_add_neg, ← support_neg g]
  exact support_add

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