Topology on filters of a space with order topology

In this file we prove that 𝓝 (f x) tends to 𝓝 Filter.atTop provided that f tends to Filter.atTop, and similarly for Filter.atBot.

theorem Filter.tendsto_nhds_atTop {X : Type u_2} [TopologicalSpace X] [PartialOrder X] [OrderTopology X] [NoMaxOrder X] : Tendsto nhds atTop (nhds atTop)

theorem Filter.tendsto_nhds_atBot {X : Type u_2} [TopologicalSpace X] [PartialOrder X] [OrderTopology X] [NoMinOrder X] : Tendsto nhds atBot (nhds atBot)

theorem Filter.Tendsto.nhds_atTop {α : Type u_1} {X : Type u_2} [TopologicalSpace X] [PartialOrder X] [OrderTopology X] [NoMaxOrder X] {f : α → X} {l : Filter α} (h : Tendsto f l atTop) : Tendsto (nhds ∘ f) l (nhds atTop)

theorem Filter.Tendsto.nhds_atBot {α : Type u_1} {X : Type u_2} [TopologicalSpace X] [PartialOrder X] [OrderTopology X] [NoMinOrder X] {f : α → X} {l : Filter α} (h : Tendsto f l atBot) : Tendsto (nhds ∘ f) l (nhds atBot)