diff --git a/Mathlib/Topology/Order/LowerUpperTopology.lean b/Mathlib/Topology/Order/LowerUpperTopology.lean
index 34ccdbc54eeb5..2f58eb8afa600 100644
--- a/Mathlib/Topology/Order/LowerUpperTopology.lean
+++ b/Mathlib/Topology/Order/LowerUpperTopology.lean
@@ -102,16 +102,32 @@ protected def rec {β : WithLower α → Sort*} (h : ∀ a, β (toLower a)) : 
 instance [Nonempty α] : Nonempty (WithLower α) := ‹Nonempty α›
 instance [Inhabited α] : Inhabited (WithLower α) := ‹Inhabited α›
 
+section Preorder
+
 variable [Preorder α] {s : Set α}
 
 instance : Preorder (WithLower α) := ‹Preorder α›
-instance : TopologicalSpace (WithLower α) := lower α
+instance : TopologicalSpace (WithLower α) := lower (WithLower α)
+
+@[simp] lemma toLower_le_toLower {x y : α} : toLower x ≤ toLower y ↔ x ≤ y := .rfl
+@[simp] lemma toLower_lt_toLower {x y : α} : toLower x < toLower y ↔ x < y := .rfl
+@[simp] lemma ofLower_le_ofLower {x y : WithLower α} : ofLower x ≤ ofLower y ↔ x ≤ y := .rfl
+@[simp] lemma ofLower_lt_ofLower {x y : WithLower α} : ofLower x < ofLower y ↔ x < y := .rfl
 
-lemma isOpen_preimage_ofLower : IsOpen (ofLower ⁻¹' s) ↔ (lower α).IsOpen s := Iff.rfl
+lemma isOpen_preimage_ofLower : IsOpen (ofLower ⁻¹' s) ↔ IsOpen[lower α] s := Iff.rfl
 
-lemma isOpen_def (T : Set (WithLower α)) : IsOpen T ↔ (lower α).IsOpen (WithLower.toLower ⁻¹' T) :=
+lemma isOpen_def (T : Set (WithLower α)) : IsOpen T ↔ IsOpen[lower α] (WithLower.toLower ⁻¹' T) :=
   Iff.rfl
 
+theorem continuous_toLower [TopologicalSpace α] [ClosedIciTopology α] :
+    Continuous (toLower : α → WithLower α) :=
+  continuous_generateFrom_iff.mpr <| by rintro _ ⟨a, rfl⟩; exact isClosed_Ici.isOpen_compl
+
+end Preorder
+
+instance [PartialOrder α] : PartialOrder (WithLower α) := ‹PartialOrder α›
+instance [LinearOrder α] : LinearOrder (WithLower α) := ‹LinearOrder α›
+
 end WithLower
 
 /-- Type synonym for a preorder equipped with the upper topology. -/
@@ -141,15 +157,31 @@ protected def rec {β : WithUpper α → Sort*} (h : ∀ a, β (toUpper a)) : 
 instance [Nonempty α] : Nonempty (WithUpper α) := ‹Nonempty α›
 instance [Inhabited α] : Inhabited (WithUpper α) := ‹Inhabited α›
 
+section Preorder
+
 variable [Preorder α] {s : Set α}
 
 instance : Preorder (WithUpper α) := ‹Preorder α›
-instance : TopologicalSpace (WithUpper α) := upper α
+instance : TopologicalSpace (WithUpper α) := upper (WithUpper α)
+
+@[simp] lemma toUpper_le_toUpper {x y : α} : toUpper x ≤ toUpper y ↔ x ≤ y := .rfl
+@[simp] lemma toUpper_lt_toUpper {x y : α} : toUpper x < toUpper y ↔ x < y := .rfl
+@[simp] lemma ofUpper_le_ofUpper {x y : WithUpper α} : ofUpper x ≤ ofUpper y ↔ x ≤ y := .rfl
+@[simp] lemma ofUpper_lt_ofUpper {x y : WithUpper α} : ofUpper x < ofUpper y ↔ x < y := .rfl
 
 lemma isOpen_preimage_ofUpper : IsOpen (ofUpper ⁻¹' s) ↔ (upper α).IsOpen s := Iff.rfl
 
 lemma isOpen_def {s : Set (WithUpper α)} : IsOpen s ↔ (upper α).IsOpen (toUpper ⁻¹' s) := Iff.rfl
 
+theorem continuous_toUpper [TopologicalSpace α] [ClosedIicTopology α] :
+    Continuous (toUpper : α → WithUpper α) :=
+  continuous_generateFrom_iff.mpr <| by rintro _ ⟨a, rfl⟩; exact isClosed_Iic.isOpen_compl
+
+end Preorder
+
+instance [PartialOrder α] : PartialOrder (WithUpper α) := ‹PartialOrder α›
+instance [LinearOrder α] : LinearOrder (WithUpper α) := ‹LinearOrder α›
+
 end WithUpper
 
 /--
@@ -236,6 +268,11 @@ theorem isLowerSet_of_isOpen (h : IsOpen s) : IsLowerSet s := by
 theorem isUpperSet_of_isClosed (h : IsClosed s) : IsUpperSet s :=
   isLowerSet_compl.1 <| isLowerSet_of_isOpen h.isOpen_compl
 
+theorem tendsto_nhds_iff_not_le {β : Type*} {f : β → α} {l : Filter β} {x : α} :
+    Filter.Tendsto f l (𝓝 x) ↔ ∀ y, ¬y ≤ x → ∀ᶠ z in l, ¬y ≤ f z := by
+  simp [topology_eq_lowerTopology, tendsto_nhds_generateFrom_iff, Filter.Eventually, Ici,
+    compl_setOf]
+
 /--
 The closure of a singleton `{a}` in the lower topology is the left-closed right-infinite interval
 [a, ∞).
@@ -292,6 +329,10 @@ lemma isTopologicalBasis_insert_univ_subbasis :
     use b ⊓ c
     rw [compl_Ici, compl_Ici, compl_Ici, Iio_inter_Iio])
 
+theorem tendsto_nhds_iff_lt {β : Type*} {f : β → α} {l : Filter β} {x : α} :
+    Filter.Tendsto f l (𝓝 x) ↔ ∀ y, x < y → ∀ᶠ z in l, f z < y := by
+  simp only [tendsto_nhds_iff_not_le, not_le]
+
 end LinearOrder
 
 section CompleteLinearOrder
@@ -382,6 +423,10 @@ theorem isUpperSet_of_isOpen (h : IsOpen s) : IsUpperSet s :=
 theorem isLowerSet_of_isClosed (h : IsClosed s) : IsLowerSet s :=
   isUpperSet_compl.1 <| isUpperSet_of_isOpen h.isOpen_compl
 
+theorem tendsto_nhds_iff_not_le {β : Type*} {f : β → α} {l : Filter β} {x : α} :
+    Filter.Tendsto f l (𝓝 x) ↔ ∀ y, ¬x ≤ y → ∀ᶠ z in l, ¬f z ≤ y :=
+  IsLower.tendsto_nhds_iff_not_le (α := αᵒᵈ)
+
 /--
 The closure of a singleton `{a}` in the upper topology is the left-infinite right-closed interval
 (-∞,a].
@@ -421,6 +466,10 @@ lemma isTopologicalBasis_insert_univ_subbasis :
     IsTopologicalBasis (insert univ {s : Set α | ∃ a, (Iic a)ᶜ = s}) :=
   IsLower.isTopologicalBasis_insert_univ_subbasis (α := αᵒᵈ)
 
+theorem tendsto_nhds_iff_lt {β : Type*} {f : β → α} {l : Filter β} {x : α} :
+    Filter.Tendsto f l (𝓝 x) ↔ ∀ y < x, ∀ᶠ z in l, y < f z :=
+  IsLower.tendsto_nhds_iff_lt (α := αᵒᵈ)
+
 end LinearOrder
 
 section CompleteLinearOrder