not_tendsto_nhds_of_tendsto_atTop

English

If a function tends to atTop along a filter, it cannot tend to any finite point in the nhds of that point.

Русский

Если функция сходится к atTop вдоль фильтра, то она не может сходиться к любой конечной точке в окрестностях этой точки.

LaTeX

$$$ \text{Tendsto } f l (atTop) \rightarrow \forall a, \lnot Tendsto f l (nhds a) $$$

Lean4

theorem not_tendsto_nhds_of_tendsto_atTop (hf : Tendsto f l atTop) (a : α) : ¬Tendsto f l (𝓝 a) :=
  hf.not_tendsto (disjoint_nhds_atTop a).symm

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