mulSupport_add_one — Mathlib

English

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

Русский

Если R — добавочно-правый отменяемый моноид, то для любой f: I → R выполняется: опора a ↦ f(a) + 1 равна опоре f.

LaTeX

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

Lean4

theorem mulSupport_add_one [AddRightCancelMonoid R] (f : ι → R) : mulSupport (fun x ↦ f x + 1) = support f :=
  Set.ext fun _ ↦ not_congr add_eq_right

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