support_neg — Mathlib

English

For a finsupp f : ι →₀ G, the support of its negation equals the support of f: supp(-f) = supp(f).

Русский

Опора отрицания функции с конечной опорой совпадает с опорой самой функции: supp(-f) = supp(f).

LaTeX

$$$\operatorname{support}(-f) = \operatorname{support}(f).$$$

Lean4

@[simp]
theorem support_neg (f : ι →₀ G) : support (-f) = support f :=
  Finset.Subset.antisymm support_mapRange
    (calc
      support f = support (- -f) := congr_arg support (neg_neg _).symm
      _ ⊆ support (-f) := support_mapRange)

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