cuspFunction_zero_eq_limUnder_nhds_ne

English

The value cuspFunction(h, f) at 0 equals the limit under nhdsWithin of 0 outside 0.

Русский

Значение cuspFunction(h, f) в 0 равно пределу в рамках nhdsWithin около 0, исключая 0.

LaTeX

$$cuspFunction(h,f)(0) = limUnder (𝓝[≠] 0) (cuspFunction(h,f))$$

Lean4

theorem cuspFunction_zero_eq_limUnder_nhds_ne : cuspFunction h f 0 = limUnder (𝓝[≠] 0) (cuspFunction h f) :=
  by
  conv_lhs => simp only [cuspFunction, update_self]
  refine congr_arg lim (Filter.map_congr <| eventuallyEq_nhdsWithin_of_eqOn fun r hr ↦ ?_)
  rw [cuspFunction, update_of_ne hr]

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