fix(Topology/Order/UpperLowerSetTopology): Fix theorem names in Upper…

…LowerSetTopology to match mathlib4 conventions (#6557)

Modify lemma names in `UpperLowerSetTopology` to meet Mathlib4 conventions.



Co-authored-by: Christopher Hoskin <mans0954@users.noreply.github.com>

Mathlib/Topology/Order/LowerUpperTopology.lean

@@ -236,7 +236,11 @@ instance [Preorder α] : LowerTopology (WithLowerTopology α) :=
 instance [Preorder α] : UpperTopology (WithUpperTopology α) :=
   ⟨rfl⟩
 
-def toOrderDualHomeomorph [Preorder α] : WithLowerTopology α ≃ₜ WithUpperTopology αᵒᵈ where
+/--
+The lower topology is homeomorphic to the upper topology on the dual order
+-/
+def WithLowerTopology.toDualHomeomorph [Preorder α] : WithLowerTopology α ≃ₜ WithUpperTopology αᵒᵈ
+    where
   toFun := OrderDual.toDual
   invFun := OrderDual.ofDual
   left_inv := OrderDual.toDual_ofDual

Mathlib/Topology/Order/UpperLowerSetTopology.lean

@@ -22,9 +22,8 @@ topology does not coincide with the lower topology.
 - `UpperSetTopology.toAlexandrovDiscrete`: The upper set topology is Alexandrov-discrete.
 - `UpperSetTopology.isClosed_iff_isLower` - a set is closed if and only if it is a Lower set
 - `UpperSetTopology.closure_eq_lowerClosure` - topological closure coincides with lower closure
-- `UpperSetTopology.Monotone_tfae` - the continuous functions are characterised as the monotone
-  functions
-- `UpperSetTopology.Monotone_to_UpperTopology_Continuous` - a `Monotone` map from a `Preorder`
+- `UpperSetTopology.monotone_iff_continuous` - the continuous functions are the monotone functions
+- `UpperSetTopology.monotone_to_upperTopology_continuous` - a `Monotone` map from a `Preorder`
   with the `UpperSetTopology` to `Preorder` with the `UpperTopology` is `Continuous`
 
 ## Implementation notes
@@ -204,7 +203,10 @@ def toLowerSetOrderIso : OrderIso α (WithLowerSetTopology α) :=
 
 end WithLowerSetTopology
 
-def UpperLowerSet_toOrderDualHomeomorph [Preorder α] :
+/--
+The Upper Set topology is homeomorphic to the Lower Set topology on the dual order
+-/
+def WithUpperSetTopology.toDualHomeomorph [Preorder α] :
     WithUpperSetTopology α ≃ₜ WithLowerSetTopology αᵒᵈ where
   toFun := OrderDual.toDual
   invFun := OrderDual.ofDual
@@ -266,16 +268,16 @@ instance instLowerSetTopologyDual [Preorder α] [TopologicalSpace α] [UpperSetT
 def withUpperSetTopologyHomeomorph : WithUpperSetTopology α ≃ₜ α :=
   WithUpperSetTopology.ofUpperSet.toHomeomorphOfInducing ⟨by erw [topology_eq α, induced_id]; rfl⟩
 
-lemma IsOpen_iff_IsUpperSet : IsOpen s ↔ IsUpperSet s := by
+lemma isOpen_iff_isUpperSet : IsOpen s ↔ IsUpperSet s := by
   rw [topology_eq α]
   rfl
 
 instance toAlexandrovDiscrete : AlexandrovDiscrete α where
-  isOpen_sInter S := by simpa only [IsOpen_iff_IsUpperSet] using isUpperSet_sInter (α := α)
+  isOpen_sInter S := by simpa only [isOpen_iff_isUpperSet] using isUpperSet_sInter (α := α)
 
 -- c.f. isClosed_iff_lower_and_subset_implies_LUB_mem
 lemma isClosed_iff_isLower {s : Set α} : IsClosed s ↔ (IsLowerSet s) := by
-  rw [← isOpen_compl_iff, IsOpen_iff_IsUpperSet,
+  rw [← isOpen_compl_iff, isOpen_iff_isUpperSet,
     isLowerSet_compl.symm, compl_compl]
 
 lemma isClosed_isLower {s : Set α} : IsClosed s → IsLowerSet s := fun h =>
@@ -310,7 +312,7 @@ protected lemma monotone_iff_continuous [TopologicalSpace α] [UpperSetTopology
     Monotone f ↔ Continuous f := by
   constructor
   · intro hf
-    simp_rw [continuous_def, IsOpen_iff_IsUpperSet]
+    simp_rw [continuous_def, isOpen_iff_isUpperSet]
     exact fun _ hs ↦ IsUpperSet.preimage hs hf
   · intro hf a b hab
     rw [← mem_Iic, ← closure_singleton] at hab ⊢
@@ -319,18 +321,18 @@ protected lemma monotone_iff_continuous [TopologicalSpace α] [UpperSetTopology
     apply closure_mono
     rw [singleton_subset_iff, mem_preimage, mem_singleton_iff]
 
-lemma Monotone_to_UpperTopology_Continuous [TopologicalSpace α]
+lemma monotone_to_upperTopology_continuous [TopologicalSpace α]
     [UpperSetTopology α] [TopologicalSpace β] [UpperTopology β] {f : α → β} (hf : Monotone f) :
     Continuous f := by
   rw [continuous_def]
   intro s hs
-  rw [IsOpen_iff_IsUpperSet]
+  rw [isOpen_iff_isUpperSet]
   apply IsUpperSet.preimage _ hf
   apply UpperTopology.isUpperSet_of_isOpen hs
 
-lemma UpperSetLEUpper {t₁ : TopologicalSpace α} [@UpperSetTopology α t₁ _]
+lemma upperSet_LE_upper {t₁ : TopologicalSpace α} [@UpperSetTopology α t₁ _]
     {t₂ : TopologicalSpace α} [@UpperTopology α t₂ _] : t₁ ≤ t₂ := fun s hs => by
-  rw [@IsOpen_iff_IsUpperSet α _ t₁]
+  rw [@isOpen_iff_isUpperSet α _ t₁]
   exact UpperTopology.isUpperSet_of_isOpen hs
 
 end maps
@@ -360,15 +362,15 @@ instance instUpperSetTopologyDual [Preorder α] [TopologicalSpace α] [LowerSetT
 def withLowerSetTopologyHomeomorph : WithLowerSetTopology α ≃ₜ α :=
   WithLowerSetTopology.ofLowerSet.toHomeomorphOfInducing ⟨by erw [topology_eq α, induced_id]; rfl⟩
 
-lemma IsOpen_iff_IsLowerSet : IsOpen s ↔ IsLowerSet s := by
+lemma isOpen_iff_isLowerSet : IsOpen s ↔ IsLowerSet s := by
   rw [topology_eq α]
   rfl
 
 instance toAlexandrovDiscrete : AlexandrovDiscrete α :=
 UpperSetTopology.toAlexandrovDiscrete (α := αᵒᵈ)
 
 lemma isClosed_iff_isUpper {s : Set α} : IsClosed s ↔ (IsUpperSet s) := by
-  rw [← isOpen_compl_iff, IsOpen_iff_IsLowerSet, isUpperSet_compl.symm, compl_compl]
+  rw [← isOpen_compl_iff, isOpen_iff_isLowerSet, isUpperSet_compl.symm, compl_compl]
 
 lemma isClosed_isUpper {s : Set α} : IsClosed s → IsUpperSet s := fun h =>
   (isClosed_iff_isUpper.mp h)
@@ -400,29 +402,29 @@ protected lemma monotone_iff_continuous [TopologicalSpace α] [LowerSetTopology
   exact UpperSetTopology.monotone_iff_continuous (α := αᵒᵈ) (β := βᵒᵈ)
     (f:= (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ))
 
-lemma Monotone_to_LowerTopology_Continuous [TopologicalSpace α]
+lemma monotone_to_lowerTopology_continuous [TopologicalSpace α]
     [LowerSetTopology α] [TopologicalSpace β] [LowerTopology β] {f : α → β} (hf : Monotone f) :
     Continuous f := by
-  apply UpperSetTopology.Monotone_to_UpperTopology_Continuous (α := αᵒᵈ) (β := βᵒᵈ)
+  apply UpperSetTopology.monotone_to_upperTopology_continuous (α := αᵒᵈ) (β := βᵒᵈ)
     (f:= (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ))
   exact Monotone.dual hf
 
-lemma LowerSetLELower {t₁ : TopologicalSpace α} [@LowerSetTopology α t₁ _]
+lemma lowerSet_LE_lower {t₁ : TopologicalSpace α} [@LowerSetTopology α t₁ _]
     {t₂ : TopologicalSpace α} [@LowerTopology α t₂ _] : t₁ ≤ t₂ := fun s hs => by
-  rw [@IsOpen_iff_IsLowerSet α _ t₁]
+  rw [@isOpen_iff_isLowerSet α _ t₁]
   exact LowerTopology.isLowerSet_of_isOpen hs
 
 end maps
 
 end LowerSetTopology
 
-lemma UpperSetDual_iff_LowerSet [Preorder α] [TopologicalSpace α] :
+lemma upperSet_dual_iff_lowerSet [Preorder α] [TopologicalSpace α] :
     UpperSetTopology αᵒᵈ ↔ LowerSetTopology α := by
   constructor
   · apply UpperSetTopology.instLowerSetTopologyDual
   · apply LowerSetTopology.instUpperSetTopologyDual
 
-lemma LowerSetDual_iff_UpperSet [Preorder α] [TopologicalSpace α] :
+lemma lowerSet_dual_iff_upperSet [Preorder α] [TopologicalSpace α] :
     LowerSetTopology αᵒᵈ ↔ UpperSetTopology α := by
   constructor
   · apply LowerSetTopology.instUpperSetTopologyDual