tendsto_nhds_atBot — Mathlib

English

In a no-min-order space, the neighborhood filter behaves continuously along the atBot direction: nhds_atBot arises as a limit.

Русский

В пространстве без минимума направление к atBot задаёт предельную кривую окрестностей.

LaTeX

$$Tendsto 𝓝 (atBot) (𝓝 atBot).$$

Lean4

protected theorem tendsto_nhds_atBot [NoMinOrder X] : Tendsto 𝓝 (atBot : Filter X) (𝓝 atBot) :=
  @Filter.tendsto_nhds_atTop Xᵒᵈ _ _ _ _

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