mulSupport_pow — Mathlib

English

For any f: α → M and n ∈ ℕ, the support of f^n is contained in the support of f.

Русский

Для любого f: α → M и натурального n, опора f^n содержится в опоре f.

LaTeX

$$For all n ∈ ℕ, \mathrm{mulSupport}(f^n) ⊆ \mathrm{mulSupport}(f)$$

Lean4

@[to_additive]
theorem mulSupport_pow [Monoid M] (f : α → M) (n : ℕ) : (mulSupport fun x => f x ^ n) ⊆ mulSupport f := by
  induction n with
  | zero => simp [pow_zero]
  | succ n hfn => simpa only [pow_succ'] using (mulSupport_mul f _).trans (union_subset Subset.rfl hfn)

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