congr — Mathlib

English

If hf is a superpolynomial decay for f and f and g agree at every point, then g also has superpolynomial decay with the same k and l.

Русский

Если hf задаёт сверхполиномиальное затухание для f и если для всех x выполняется f(x) = g(x), то и g имеет сверхполиномиальное затухание.

LaTeX

$$$\mathrm{SuperpolynomialDecay}(l,k,f) \wedge (\forall x, f(x)=g(x)) \Rightarrow \mathrm{SuperpolynomialDecay}(l,k,g)$$$

Lean4

theorem congr (hf : SuperpolynomialDecay l k f) (hfg : ∀ x, f x = g x) : SuperpolynomialDecay l k g := fun z =>
  (hf z).congr fun x => (congr_arg fun a => k x ^ z * a) <| hfg x

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