support_pow — Mathlib

English

For a function f: ι → M₀ and a nonzero n, the support of the nth power map a ↦ f(a)^n equals the support of f; i.e., supp(a ↦ f(a)^n) = supp(f).

Русский

Для функции f: ι → M₀ и не нулевого n опора функции a ↦ f(a)^n равна опоре f.

LaTeX

$$$ \operatorname{support}(a \mapsto f(a)^n) = \operatorname{support}(f). $$$

Lean4

@[simp]
theorem support_pow (f : ι → M₀) (hn : n ≠ 0) : support (fun a ↦ f a ^ n) = support f := by ext;
  exact (pow_eq_zero_iff hn).not

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