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]
:
Filter.Tendsto nhds Filter.atTop (nhds Filter.atTop)
theorem
Filter.tendsto_nhds_atBot
{X : Type u_2}
[TopologicalSpace X]
[PartialOrder X]
[OrderTopology X]
[NoMinOrder X]
:
Filter.Tendsto nhds Filter.atBot (nhds Filter.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 : Filter.Tendsto f l Filter.atTop)
:
Filter.Tendsto (nhds ∘ f) l (nhds Filter.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 : Filter.Tendsto f l Filter.atBot)
:
Filter.Tendsto (nhds ∘ f) l (nhds Filter.atBot)