cuspFunction_zero_of_zero_at_inf — Mathlib

English

If h > 0 and f has a zero-at-infinity property, cuspFunction(h,f) at 0 equals 0.

Русский

Если h > 0 и f имеет нуль-ат бесконечности, cuspFunction(h,f) в 0 равно 0.

LaTeX

$$hh > 0 ∧ ZeroAtFilter I∞ f → cuspFunction(h,f)(0) = 0$$

Lean4

theorem cuspFunction_zero_of_zero_at_inf (hh : 0 < h) (h_zer : ZeroAtFilter I∞ f) : cuspFunction h f 0 = 0 := by
  simpa only [cuspFunction, update_self] using (h_zer.comp (invQParam_tendsto hh)).limUnder_eq

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