mulSupport_one_sub' — Mathlib

English

If R is an AddGroup, then for any f: I → R, the support of the function a ↦ 1 − f(a) equals the support of f.

Русский

Если R — аддитивная группа, то для любой f: I → R опора a ↦ 1 − f(a) равна опоре f.

LaTeX

$$$\\operatorname{mulSupport}(1 - f) = \\operatorname{support}(f)$$$

Lean4

theorem mulSupport_one_sub' [AddGroup R] (f : ι → R) : mulSupport (1 - f) = support f := by
  rw [sub_eq_add_neg, mulSupport_one_add', support_neg]

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