chore(topology/order/basic): split (#18363)

Move material that requires topological groups to a new file to reduce transitive imports.

src/analysis/box_integral/partition/basic.lean

@@ -3,6 +3,7 @@ Copyright (c) 2021 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
+import algebra.big_operators.option
 import analysis.box_integral.box.basic
 
 /-!

src/analysis/convex/strict.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
 import analysis.convex.basic
-import topology.order.basic
+import topology.algebra.order.group
 
 /-!
 # Strictly convex sets

src/topology/algebra/monoid.lean

@@ -49,6 +49,8 @@ section has_continuous_mul
 
 variables [topological_space M] [has_mul M] [has_continuous_mul M]
 
+@[to_additive] instance : has_continuous_mul Mᵒᵈ := ‹has_continuous_mul M›
+
 @[to_additive]
 lemma continuous_mul : continuous (λp:M×M, p.1 * p.2) :=
 has_continuous_mul.continuous_mul

src/topology/algebra/order/field.lean

@@ -5,7 +5,7 @@ Authors: Benjamin Davidson, Devon Tuma, Eric Rodriguez, Oliver Nash
 -/
 
 import tactic.positivity
-import topology.order.basic
+import topology.algebra.order.group
 import topology.algebra.field
 
 /-!

src/topology/algebra/order/floor.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Anatole Dedecker
 -/
 import algebra.order.floor
-import topology.order.basic
+import topology.algebra.order.group
 
 /-!
 # Topological facts about `int.floor`, `int.ceil` and `int.fract`
@@ -156,7 +156,7 @@ tendsto_nhds_within_of_tendsto_nhds_of_eventually_within _
 
 local notation `I` := (Icc 0 1 : set α)
 
-variables [order_topology α] [topological_add_group α] [topological_space β] [topological_space γ]
+variables [order_topology α] [topological_space β] [topological_space γ]
 
 /-- Do not use this, use `continuous_on.comp_fract` instead. -/
 lemma continuous_on.comp_fract' {f : β → α → γ}

src/topology/algebra/order/group.lean

@@ -0,0 +1,80 @@
+/-
+Copyright (c) 2020 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov
+-/
+import topology.order.basic
+import topology.algebra.group.basic
+
+/-!
+# Topology on a linear ordered additive commutative group
+
+In this file we prove that a linear ordered additive commutative group with order topology is a
+topological group. We also prove continuity of `abs : G → G` and provide convenience lemmas like
+`continuous_at.abs`.
+-/
+
+open set filter
+open_locale topology filter
+
+variables {α G : Type*} [topological_space G] [linear_ordered_add_comm_group G] [order_topology G]
+variables {l : filter α} {f g : α → G}
+
+@[priority 100] -- see Note [lower instance priority]
+instance linear_ordered_add_comm_group.topological_add_group : topological_add_group G :=
+{ continuous_add :=
+    begin
+      refine continuous_iff_continuous_at.2 _,
+      rintro ⟨a, b⟩,
+      refine linear_ordered_add_comm_group.tendsto_nhds.2 (λ ε ε0, _),
+      rcases dense_or_discrete 0 ε with (⟨δ, δ0, δε⟩|⟨h₁, h₂⟩),
+      { -- If there exists `δ ∈ (0, ε)`, then we choose `δ`-nhd of `a` and `(ε-δ)`-nhd of `b`
+        filter_upwards [(eventually_abs_sub_lt a δ0).prod_nhds
+          (eventually_abs_sub_lt b (sub_pos.2 δε))],
+        rintros ⟨x, y⟩ ⟨hx : |x - a| < δ, hy : |y - b| < ε - δ⟩,
+        rw [add_sub_add_comm],
+        calc |x - a + (y - b)| ≤ |x - a| + |y - b| : abs_add _ _
+        ... < δ + (ε - δ) : add_lt_add hx hy
+        ... = ε : add_sub_cancel'_right _ _ },
+      { -- Otherwise `ε`-nhd of each point `a` is `{a}`
+        have hε : ∀ {x y}, |x - y| < ε → x = y,
+        { intros x y h,
+          simpa [sub_eq_zero] using h₂ _ h },
+        filter_upwards [(eventually_abs_sub_lt a ε0).prod_nhds (eventually_abs_sub_lt b ε0)],
+        rintros ⟨x, y⟩ ⟨hx : |x - a| < ε, hy : |y - b| < ε⟩,
+        simpa [hε hx, hε hy] }
+    end,
+  continuous_neg := continuous_iff_continuous_at.2 $ λ a,
+    linear_ordered_add_comm_group.tendsto_nhds.2 $ λ ε ε0,
+      (eventually_abs_sub_lt a ε0).mono $ λ x hx, by rwa [neg_sub_neg, abs_sub_comm] }
+
+@[continuity]
+lemma continuous_abs : continuous (abs : G → G) := continuous_id.max continuous_neg
+
+protected lemma filter.tendsto.abs {a : G} (h : tendsto f l (𝓝 a)) :
+  tendsto (λ x, |f x|) l (𝓝 (|a|)) :=
+(continuous_abs.tendsto _).comp h
+
+lemma tendsto_zero_iff_abs_tendsto_zero (f : α → G) :
+  tendsto f l (𝓝 0) ↔ tendsto (abs ∘ f) l (𝓝 0) :=
+begin
+  refine ⟨λ h, (abs_zero : |(0 : G)| = 0) ▸ h.abs, λ h, _⟩,
+  have : tendsto (λ a, -|f a|) l (𝓝 0) := (neg_zero : -(0 : G) = 0) ▸ h.neg,
+  exact tendsto_of_tendsto_of_tendsto_of_le_of_le this h
+    (λ x, neg_abs_le_self $ f x) (λ x, le_abs_self $ f x),
+end
+
+variables [topological_space α] {a : α} {s : set α}
+
+protected lemma continuous.abs (h : continuous f) : continuous (λ x, |f x|) := continuous_abs.comp h
+
+protected lemma continuous_at.abs (h : continuous_at f a) : continuous_at (λ x, |f x|) a := h.abs
+
+protected lemma continuous_within_at.abs (h : continuous_within_at f s a) :
+  continuous_within_at (λ x, |f x|) s a := h.abs
+
+protected lemma continuous_on.abs (h : continuous_on f s) : continuous_on (λ x, |f x|) s :=
+λ x hx, (h x hx).abs
+
+lemma tendsto_abs_nhds_within_zero : tendsto (abs : G → G) (𝓝[≠] 0) (𝓝[>] 0) :=
+(continuous_abs.tendsto' (0 : G) 0 abs_zero).inf $ tendsto_principal_principal.2 $ λ x, abs_pos.2

src/topology/algebra/order/liminf_limsup.lean

@@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro, Yury Kudryashov
 -/
 import algebra.big_operators.intervals
+import algebra.big_operators.order
+import algebra.indicator_function
 import order.liminf_limsup
 import order.filter.archimedean
 import topology.order.basic

src/topology/algebra/order/monotone_continuity.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury G. Kudryashov, Heather Macbeth
 -/
 import topology.order.basic
-import topology.algebra.order.left_right
+import topology.homeomorph
 
 /-!
 # Continuity of monotone functions

src/topology/continuous_function/ordered.lean

@@ -5,6 +5,7 @@ Authors: Scott Morrison, Shing Tak Lam
 -/
 
 import topology.algebra.order.proj_Icc
+import topology.algebra.order.group
 import topology.continuous_function.basic
 
 /-!

src/topology/order/basic.lean

@@ -6,7 +6,7 @@ Authors: Johannes Hölzl, Mario Carneiro, Yury Kudryashov
 import data.set.intervals.pi
 import data.set.pointwise.interval
 import order.filter.interval
-import topology.algebra.group.basic
+import topology.support
 import topology.algebra.order.left_right
 
 /-!
@@ -94,9 +94,6 @@ instance [topological_space α] [h : first_countable_topology α] : first_counta
 instance [topological_space α] [h : second_countable_topology α] : second_countable_topology αᵒᵈ :=
 h
 
-@[to_additive]
-instance [topological_space α] [has_mul α] [h : has_continuous_mul α] : has_continuous_mul αᵒᵈ := h
-
 lemma dense.order_dual [topological_space α] {s : set α} (hs : dense s) :
   dense (order_dual.of_dual ⁻¹' s) := hs
 
@@ -1608,6 +1605,7 @@ end order_topology
 end linear_order
 
 section linear_ordered_add_comm_group
+
 variables [topological_space α] [linear_ordered_add_comm_group α] [order_topology α]
 variables {l : filter β} {f g : β → α}
 
@@ -1643,50 +1641,35 @@ lemma eventually_abs_sub_lt (a : α) {ε : α} (hε : 0 < ε) : ∀ᶠ x in 𝓝
 (nhds_eq_infi_abs_sub a).symm ▸ mem_infi_of_mem ε
   (mem_infi_of_mem hε $ by simp only [abs_sub_comm, mem_principal_self])
 
-@[priority 100] -- see Note [lower instance priority]
-instance linear_ordered_add_comm_group.topological_add_group : topological_add_group α :=
-{ continuous_add :=
-    begin
-      refine continuous_iff_continuous_at.2 _,
-      rintro ⟨a, b⟩,
-      refine linear_ordered_add_comm_group.tendsto_nhds.2 (λ ε ε0, _),
-      rcases dense_or_discrete 0 ε with (⟨δ, δ0, δε⟩|⟨h₁, h₂⟩),
-      { -- If there exists `δ ∈ (0, ε)`, then we choose `δ`-nhd of `a` and `(ε-δ)`-nhd of `b`
-        filter_upwards [(eventually_abs_sub_lt a δ0).prod_nhds
-          (eventually_abs_sub_lt b (sub_pos.2 δε))],
-        rintros ⟨x, y⟩ ⟨hx : |x - a| < δ, hy : |y - b| < ε - δ⟩,
-        rw [add_sub_add_comm],
-        calc |x - a + (y - b)| ≤ |x - a| + |y - b| : abs_add _ _
-        ... < δ + (ε - δ) : add_lt_add hx hy
-        ... = ε : add_sub_cancel'_right _ _ },
-      { -- Otherwise `ε`-nhd of each point `a` is `{a}`
-        have hε : ∀ {x y}, |x - y| < ε → x = y,
-        { intros x y h,
-          simpa [sub_eq_zero] using h₂ _ h },
-        filter_upwards [(eventually_abs_sub_lt a ε0).prod_nhds (eventually_abs_sub_lt b ε0)],
-        rintros ⟨x, y⟩ ⟨hx : |x - a| < ε, hy : |y - b| < ε⟩,
-        simpa [hε hx, hε hy] }
-    end,
-  continuous_neg := continuous_iff_continuous_at.2 $ λ a,
-    linear_ordered_add_comm_group.tendsto_nhds.2 $ λ ε ε0,
-      (eventually_abs_sub_lt a ε0).mono $ λ x hx, by rwa [neg_sub_neg, abs_sub_comm] }
-
-@[continuity]
-lemma continuous_abs : continuous (abs : α → α) := continuous_id.max continuous_neg
-
-lemma filter.tendsto.abs {f : β → α} {a : α} {l : filter β} (h : tendsto f l (𝓝 a)) :
-  tendsto (λ x, |f x|) l (𝓝 (|a|)) :=
-(continuous_abs.tendsto _).comp h
-
-lemma tendsto_zero_iff_abs_tendsto_zero (f : β → α) {l : filter β} :
-  tendsto f l (𝓝 0) ↔ tendsto (abs ∘ f) l (𝓝 0) :=
+/-- In a linearly ordered additive commutative group with the order topology, if `f` tends to `C`
+and `g` tends to `at_top` then `f + g` tends to `at_top`. -/
+lemma filter.tendsto.add_at_top {C : α} (hf : tendsto f l (𝓝 C)) (hg : tendsto g l at_top) :
+  tendsto (λ x, f x + g x) l at_top :=
 begin
-  refine ⟨λ h, (abs_zero : |(0 : α)| = 0) ▸ h.abs, λ h, _⟩,
-  have : tendsto (λ a, -|f a|) l (𝓝 0) := (neg_zero : -(0 : α) = 0) ▸ h.neg,
-  exact tendsto_of_tendsto_of_tendsto_of_le_of_le this h
-    (λ x, neg_abs_le_self $ f x) (λ x, le_abs_self $ f x),
+  nontriviality α,
+  obtain ⟨C', hC'⟩ : ∃ C', C' < C := exists_lt C,
+  refine tendsto_at_top_add_left_of_le' _ C' _ hg,
+  exact (hf.eventually (lt_mem_nhds hC')).mono (λ x, le_of_lt)
 end
 
+/-- In a linearly ordered additive commutative group with the order topology, if `f` tends to `C`
+and `g` tends to `at_bot` then `f + g` tends to `at_bot`. -/
+lemma filter.tendsto.add_at_bot {C : α} (hf : tendsto f l (𝓝 C)) (hg : tendsto g l at_bot) :
+  tendsto (λ x, f x + g x) l at_bot :=
+@filter.tendsto.add_at_top αᵒᵈ _ _ _ _ _ _ _ _ hf hg
+
+/-- In a linearly ordered additive commutative group with the order topology, if `f` tends to
+`at_top` and `g` tends to `C` then `f + g` tends to `at_top`. -/
+lemma filter.tendsto.at_top_add {C : α} (hf : tendsto f l at_top) (hg : tendsto g l (𝓝 C)) :
+  tendsto (λ x, f x + g x) l at_top :=
+by { conv in (_ + _) { rw add_comm }, exact hg.add_at_top hf }
+
+/-- In a linearly ordered additive commutative group with the order topology, if `f` tends to
+`at_bot` and `g` tends to `C` then `f + g` tends to `at_bot`. -/
+lemma filter.tendsto.at_bot_add {C : α} (hf : tendsto f l at_bot) (hg : tendsto g l (𝓝 C)) :
+  tendsto (λ x, f x + g x) l at_bot :=
+by { conv in (_ + _) { rw add_comm }, exact hg.add_at_bot hf }
+
 lemma nhds_basis_Ioo_pos [no_min_order α] [no_max_order α] (a : α) :
   (𝓝 a).has_basis (λ ε : α, (0 : α) < ε) (λ ε, Ioo (a-ε) (a+ε)) :=
 ⟨begin
@@ -1729,54 +1712,6 @@ lemma nhds_basis_Ioo_pos_of_pos [no_min_order α] [no_max_order α]
     (sub_le_sub_left (min_le_left i a) a) (add_le_add_left (min_le_left i a) a)) hit⟩,
   λ h, let ⟨i, hi, hit⟩ := h in ⟨i, hi.1, hit⟩ ⟩ ⟩
 
-section
-
-variables [topological_space β] {b : β} {a : α} {s : set β}
-
-lemma continuous.abs (h : continuous f) : continuous (λ x, |f x|) := continuous_abs.comp h
-
-lemma continuous_at.abs (h : continuous_at f b) : continuous_at (λ x, |f x|) b := h.abs
-
-lemma continuous_within_at.abs (h : continuous_within_at f s b) :
-  continuous_within_at (λ x, |f x|) s b := h.abs
-
-lemma continuous_on.abs (h : continuous_on f s) : continuous_on (λ x, |f x|) s :=
-λ x hx, (h x hx).abs
-
-lemma tendsto_abs_nhds_within_zero : tendsto (abs : α → α) (𝓝[≠] 0) (𝓝[>] 0) :=
-(continuous_abs.tendsto' (0 : α) 0 abs_zero).inf $ tendsto_principal_principal.2 $ λ x, abs_pos.2
-
-end
-
-/-- In a linearly ordered additive commutative group with the order topology, if `f` tends to `C`
-and `g` tends to `at_top` then `f + g` tends to `at_top`. -/
-lemma filter.tendsto.add_at_top {C : α} (hf : tendsto f l (𝓝 C)) (hg : tendsto g l at_top) :
-  tendsto (λ x, f x + g x) l at_top :=
-begin
-  nontriviality α,
-  obtain ⟨C', hC'⟩ : ∃ C', C' < C := exists_lt C,
-  refine tendsto_at_top_add_left_of_le' _ C' _ hg,
-  exact (hf.eventually (lt_mem_nhds hC')).mono (λ x, le_of_lt)
-end
-
-/-- In a linearly ordered additive commutative group with the order topology, if `f` tends to `C`
-and `g` tends to `at_bot` then `f + g` tends to `at_bot`. -/
-lemma filter.tendsto.add_at_bot {C : α} (hf : tendsto f l (𝓝 C)) (hg : tendsto g l at_bot) :
-  tendsto (λ x, f x + g x) l at_bot :=
-@filter.tendsto.add_at_top αᵒᵈ _ _ _ _ _ _ _ _ hf hg
-
-/-- In a linearly ordered additive commutative group with the order topology, if `f` tends to
-`at_top` and `g` tends to `C` then `f + g` tends to `at_top`. -/
-lemma filter.tendsto.at_top_add {C : α} (hf : tendsto f l at_top) (hg : tendsto g l (𝓝 C)) :
-  tendsto (λ x, f x + g x) l at_top :=
-by { conv in (_ + _) { rw add_comm }, exact hg.add_at_top hf }
-
-/-- In a linearly ordered additive commutative group with the order topology, if `f` tends to
-`at_bot` and `g` tends to `C` then `f + g` tends to `at_bot`. -/
-lemma filter.tendsto.at_bot_add {C : α} (hf : tendsto f l at_bot) (hg : tendsto g l (𝓝 C)) :
-  tendsto (λ x, f x + g x) l at_bot :=
-by { conv in (_ + _) { rw add_comm }, exact hg.add_at_bot hf }
-
 end linear_ordered_add_comm_group
 
 lemma preimage_neg [add_group α] : preimage (has_neg.neg : α → α) = image (has_neg.neg : α → α) :=
@@ -2693,18 +2628,15 @@ section nhds_with_pos
 
 section linear_ordered_add_comm_group
 
-variables [linear_ordered_add_comm_group α] [topological_space α] [order_topology α]
+variables [linear_order α] [has_zero α] [topological_space α] [order_topology α]
 
 lemma eventually_nhds_within_pos_mem_Ioo {ε : α} (h : 0 < ε) :
   ∀ᶠ x in 𝓝[>] 0, x ∈ Ioo 0 ε :=
-begin
-  rw [eventually_iff, mem_nhds_within],
-  exact ⟨Ioo (-ε) ε, is_open_Ioo, by simp [h], λ x hx, ⟨hx.2, hx.1.2⟩⟩,
-end
+Ioo_mem_nhds_within_Ioi (left_mem_Ico.2 h)
 
 lemma eventually_nhds_within_pos_mem_Ioc {ε : α} (h : 0 < ε) :
   ∀ᶠ x in 𝓝[>] 0, x ∈ Ioc 0 ε :=
-(eventually_nhds_within_pos_mem_Ioo h).mono Ioo_subset_Ioc_self
+Ioc_mem_nhds_within_Ioi (left_mem_Ico.2 h)
 
 end linear_ordered_add_comm_group
 

src/topology/order/lower_topology.lean

@@ -3,6 +3,7 @@ Copyright (c) 2023 Christopher Hoskin. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Christopher Hoskin
 -/
+import topology.homeomorph
 import topology.order.lattice
 import order.hom.complete_lattice