Topology on filters of a space with order topology #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
In this file we prove that 𝓝 (f x) tends to 𝓝 filter.at_top provided that f tends to
filter.at_top, and similarly for filter.at_bot.
@[protected]
theorem
filter.tendsto_nhds_at_top
{X : Type u_2}
[topological_space X]
[partial_order X]
[order_topology X]
[no_max_order X] :
@[protected]
theorem
filter.tendsto_nhds_at_bot
{X : Type u_2}
[topological_space X]
[partial_order X]
[order_topology X]
[no_min_order X] :
theorem
filter.tendsto.nhds_at_top
{α : Type u_1}
{X : Type u_2}
[topological_space X]
[partial_order X]
[order_topology X]
[no_max_order X]
{f : α → X}
{l : filter α}
(h : filter.tendsto f l filter.at_top) :
filter.tendsto (nhds ∘ f) l (nhds filter.at_top)
theorem
filter.tendsto.nhds_at_bot
{α : Type u_1}
{X : Type u_2}
[topological_space X]
[partial_order X]
[order_topology X]
[no_min_order X]
{f : α → X}
{l : filter α}
(h : filter.tendsto f l filter.at_bot) :
filter.tendsto (nhds ∘ f) l (nhds filter.at_bot)