congr' — Mathlib

English

Let hf be a superpolynomial decay with respect to l, k, f, and suppose f is eventually equal to g along l. Then g also has superpolynomial decay along l with the same k.

Русский

Пусть hf задаёт сверхполиномиальное затухание по отношению к l, k, f, и если f эквивалентно g по отношению к l после некоторого момента, то и g имеет то же сверхполиномиальное затухание.

LaTeX

$$$\mathrm{SuperpolynomialDecay}(l,k,f) \wedge f =^\!{l} g \;\Rightarrow\; \mathrm{SuperpolynomialDecay}(l,k,g)$$$

Lean4

theorem congr' (hf : SuperpolynomialDecay l k f) (hfg : f =ᶠ[l] g) : SuperpolynomialDecay l k g := fun z =>
  (hf z).congr' (EventuallyEq.mul (EventuallyEq.refl l _) hfg)

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