From 0796b6a7c6ff8aae8b1338018b21aaeec6c3e88e Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Fri, 10 Feb 2023 02:15:39 +0000
Subject: [PATCH] feat: port Topology.Algebra.Order.Filter (#2167)

---
 Mathlib.lean                               |  1 +
 Mathlib/Topology/Algebra/Order/Filter.lean | 46 ++++++++++++++++++++++
 2 files changed, 47 insertions(+)
 create mode 100644 Mathlib/Topology/Algebra/Order/Filter.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 8ce5ce8268e4f..c7752d2e6930b 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -1012,6 +1012,7 @@ import Mathlib.Topology.Algebra.Order.Archimedean
 import Mathlib.Topology.Algebra.Order.Compact
 import Mathlib.Topology.Algebra.Order.ExtendFrom
 import Mathlib.Topology.Algebra.Order.ExtrClosure
+import Mathlib.Topology.Algebra.Order.Filter
 import Mathlib.Topology.Algebra.Order.IntermediateValue
 import Mathlib.Topology.Algebra.Order.LeftRight
 import Mathlib.Topology.Algebra.Order.LiminfLimsup
diff --git a/Mathlib/Topology/Algebra/Order/Filter.lean b/Mathlib/Topology/Algebra/Order/Filter.lean
new file mode 100644
index 0000000000000..aafbe71370c84
--- /dev/null
+++ b/Mathlib/Topology/Algebra/Order/Filter.lean
@@ -0,0 +1,46 @@
+/-
+Copyright (c) 2022 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov
+
+! This file was ported from Lean 3 source module topology.algebra.order.filter
+! leanprover-community/mathlib commit 98e83c3d541c77cdb7da20d79611a780ff8e7d90
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.Topology.Order.Basic
+import Mathlib.Topology.Filter
+
+/-!
+# 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`.
+-/
+
+
+open Topology
+
+namespace Filter
+
+variable {α X : Type _} [TopologicalSpace X] [PartialOrder X] [OrderTopology X]
+
+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
+#align filter.tendsto_nhds_at_top Filter.tendsto_nhds_atTop
+
+protected theorem tendsto_nhds_atBot [NoMinOrder X] : Tendsto 𝓝 (atBot : Filter X) (𝓝 atBot) :=
+  @Filter.tendsto_nhds_atTop Xᵒᵈ _ _ _ _
+#align filter.tendsto_nhds_at_bot Filter.tendsto_nhds_atBot
+
+theorem Tendsto.nhds_atTop [NoMaxOrder X] {f : α → X} {l : Filter α} (h : Tendsto f l atTop) :
+    Tendsto (𝓝 ∘ f) l (𝓝 atTop) :=
+  Filter.tendsto_nhds_atTop.comp h
+#align filter.tendsto.nhds_at_top Filter.Tendsto.nhds_atTop
+
+theorem Tendsto.nhds_atBot [NoMinOrder X] {f : α → X} {l : Filter α} (h : Tendsto f l atBot) :
+    Tendsto (𝓝 ∘ f) l (𝓝 atBot) :=
+  @Tendsto.nhds_atTop α Xᵒᵈ _ _ _ _ _ _ h
+#align filter.tendsto.nhds_at_bot Filter.Tendsto.nhds_atBot
+
+end Filter