fun_pow_const — Mathlib

English

If f =^l g, then f^c =^l g^c for any exponent c when β has a Pow structure.

Русский

Если f =^l g, то f^c =^l g^c для любого показателя мощности c при наличии структуры степени.

LaTeX

$$$\\\\forall f,g : \\\\alpha \\\\to \\\\beta \\\\forall l \\\\ (l : Filter \\\\alpha), \\\\forall c \\\\in \\\\gamma, \\\\ (f =^l g) \\\\Rightarrow \\\\bigl((f)^c =^l (g)^c\\\\bigr)$$$

Lean4

@[to_additive (attr := to_additive) fun_const_smul]
theorem fun_pow_const {γ} [Pow β γ] {f g : α → β} {l : Filter α} (h : f =ᶠ[l] g) (c : γ) :
    (fun x => f x ^ c) =ᶠ[l] fun x => g x ^ c :=
  h.pow_const c

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