superpolynomialDecay_zero — Mathlib

English

The zero function decays superpolynomially along any filter and parameter if β is a topological semiring with multiplication by zero behaving regularly.

Русский

Нулевая функция имеет сверхполиномиальное затухание вдоль любого фильтра; умножение на нуль сохраняет затухание.

LaTeX

$$$\mathrm{SuperpolynomialDecay}(l,k,0)$$$

Lean4

@[simp]
theorem superpolynomialDecay_zero (l : Filter α) (k : α → β) : SuperpolynomialDecay l k 0 := fun z => by
  simpa only [Pi.zero_apply, mul_zero] using tendsto_const_nhds

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