tendsto_nhds_atTop — Mathlib

English

In a no-max-order space, the neighborhood filter behaves continuously along the atTop direction: nhds_atTop arises as a limit.

Русский

В пространстве без максимального элемента окрестности ведут себя непрерывно по направлению к atTop.

LaTeX

$$Tendsto 𝓝 (atTop) (𝓝 atTop).$$

Lean4

protected theorem tendsto_nhds_atTop [NoMaxOrder X] : Tendsto 𝓝 (atTop : Filter X) (𝓝 atTop) :=
  Filter.tendsto_nhds_atTop_iff.2 fun x => (eventually_gt_atTop x).mono fun _ => le_mem_nhds

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