boundedAtFilter_cuspFunction — Mathlib

English

If f is bounded in the infinity neighborhood, cuspFunction is bounded in the neighborhood near 0 excluding 0.

Русский

Если f ограничена около бесконечности, cuspFunction ограничена около 0, за исключением 0.

LaTeX

$$If BoundedAtFilter I∞ f then BoundedAtFilter (𝓝[≠] 0) (cuspFunction h f)$$

Lean4

theorem boundedAtFilter_cuspFunction (hh : 0 < h) (h_bd : BoundedAtFilter I∞ f) :
    BoundedAtFilter (𝓝[≠] 0) (cuspFunction h f) :=
  by
  refine (h_bd.comp_tendsto <| invQParam_tendsto hh).congr' ?_ (by simp)
  refine eventually_nhdsWithin_of_forall fun q hq ↦ ?_
  rw [cuspFunction_eq_of_nonzero _ _ hq, comp_def]

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