refactor(topology/algebra/ordered): reduce imports (#7601)

Renames `topology.algebra.ordered` to `topology.algebra.order`, and moves the material about `liminf/limsup` and about `extend_from` to separate files, in order to delay imports.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/algebra/continued_fractions/computation/approximation_corollaries.lean

@@ -5,7 +5,7 @@ Authors: Kevin Kappelmann
 -/
 import algebra.continued_fractions.computation.approximations
 import algebra.continued_fractions.convergents_equiv
-import topology.algebra.ordered
+import topology.algebra.ordered.basic
 /-!
 # Corollaries From Approximation Lemmas (`algebra.continued_fractions.computation.approximations`)
 

src/analysis/calculus/local_extr.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
 import topology.local_extr
+import topology.algebra.ordered.extend_from
 import analysis.calculus.deriv
 
 /-!

src/analysis/normed_space/basic.lean

@@ -7,6 +7,7 @@ import topology.instances.nnreal
 import topology.algebra.module
 import topology.algebra.algebra
 import topology.metric_space.antilipschitz
+import topology.algebra.ordered.liminf_limsup
 
 /-!
 # Normed spaces

src/topology/algebra/floor_ring.lean

@@ -6,7 +6,7 @@ Authors: Anatole Dedecker
 Basic topological facts (limits and continuity) about `floor`,
 `ceil` and `fract` in a `floor_ring`.
 -/
-import topology.algebra.ordered
+import topology.algebra.ordered.basic
 import algebra.floor
 
 open set function filter

src/topology/algebra/ordered.lean → src/topology/algebra/ordered/basic.lean

@@ -4,11 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro, Yury Kudryashov
 -/
 import tactic.tfae
-import algebra.archimedean
-import order.liminf_limsup
+import algebra.group_with_zero.power
 import data.set.intervals.pi
 import topology.algebra.group
-import topology.extend_from_subset
 import order.filter.interval
 
 /-!
@@ -95,7 +93,7 @@ for specific types.
 -/
 
 open classical set filter topological_space
-open function (curry uncurry)
+open function
 open_locale topological_space classical filter
 
 universes u v w
@@ -1115,7 +1113,7 @@ section pi
 /-!
 ### Intervals in `Π i, π i` belong to `𝓝 x`
 
-For each leamma `pi_Ixx_mem_nhds` we add a non-dependent version `pi_Ixx_mem_nhds'` because
+For each lemma `pi_Ixx_mem_nhds` we add a non-dependent version `pi_Ixx_mem_nhds'` because
 sometimes Lean fails to unify different instances while trying to apply the dependent version to,
 e.g., `ι → ℝ`.
 -/
@@ -2782,137 +2780,6 @@ lemma continuous.exists_forall_ge {α : Type*} [topological_space α] [nonempty
 
 end conditionally_complete_linear_order
 
-section liminf_limsup
-
-section order_closed_topology
-variables [semilattice_sup α] [topological_space α] [order_topology α]
-
-lemma is_bounded_le_nhds (a : α) : (𝓝 a).is_bounded (≤) :=
-match forall_le_or_exists_lt_sup a with
-| or.inl h := ⟨a, eventually_of_forall h⟩
-| or.inr ⟨b, hb⟩ := ⟨b, ge_mem_nhds hb⟩
-end
-
-lemma filter.tendsto.is_bounded_under_le {f : filter β} {u : β → α} {a : α}
-  (h : tendsto u f (𝓝 a)) : f.is_bounded_under (≤) u :=
-(is_bounded_le_nhds a).mono h
-
-lemma is_cobounded_ge_nhds (a : α) : (𝓝 a).is_cobounded (≥) :=
-(is_bounded_le_nhds a).is_cobounded_flip
-
-lemma filter.tendsto.is_cobounded_under_ge {f : filter β} {u : β → α} {a : α}
-  [ne_bot f] (h : tendsto u f (𝓝 a)) : f.is_cobounded_under (≥) u :=
-h.is_bounded_under_le.is_cobounded_flip
-
-end order_closed_topology
-
-section order_closed_topology
-variables [semilattice_inf α] [topological_space α] [order_topology α]
-
-lemma is_bounded_ge_nhds (a : α) : (𝓝 a).is_bounded (≥) :=
-@is_bounded_le_nhds (order_dual α) _ _ _ a
-
-lemma filter.tendsto.is_bounded_under_ge {f : filter β} {u : β → α} {a : α}
-  (h : tendsto u f (𝓝 a)) : f.is_bounded_under (≥) u :=
-(is_bounded_ge_nhds a).mono h
-
-lemma is_cobounded_le_nhds (a : α) : (𝓝 a).is_cobounded (≤) :=
-(is_bounded_ge_nhds a).is_cobounded_flip
-
-lemma filter.tendsto.is_cobounded_under_le {f : filter β} {u : β → α} {a : α}
-  [ne_bot f] (h : tendsto u f (𝓝 a)) : f.is_cobounded_under (≤) u :=
-h.is_bounded_under_ge.is_cobounded_flip
-
-end order_closed_topology
-
-section conditionally_complete_linear_order
-variables [conditionally_complete_linear_order α]
-
-theorem lt_mem_sets_of_Limsup_lt {f : filter α} {b} (h : f.is_bounded (≤)) (l : f.Limsup < b) :
-  ∀ᶠ a in f, a < b :=
-let ⟨c, (h : ∀ᶠ a in f, a ≤ c), hcb⟩ := exists_lt_of_cInf_lt h l in
-mem_sets_of_superset h $ assume a hac, lt_of_le_of_lt hac hcb
-
-theorem gt_mem_sets_of_Liminf_gt : ∀ {f : filter α} {b}, f.is_bounded (≥) → b < f.Liminf →
-  ∀ᶠ a in f, b < a :=
-@lt_mem_sets_of_Limsup_lt (order_dual α) _
-
-variables [topological_space α] [order_topology α]
-
-/-- If the liminf and the limsup of a filter coincide, then this filter converges to
-their common value, at least if the filter is eventually bounded above and below. -/
-theorem le_nhds_of_Limsup_eq_Liminf {f : filter α} {a : α}
-  (hl : f.is_bounded (≤)) (hg : f.is_bounded (≥)) (hs : f.Limsup = a) (hi : f.Liminf = a) :
-  f ≤ 𝓝 a :=
-tendsto_order.2 $ and.intro
-  (assume b hb, gt_mem_sets_of_Liminf_gt hg $ hi.symm ▸ hb)
-  (assume b hb, lt_mem_sets_of_Limsup_lt hl $ hs.symm ▸ hb)
-
-theorem Limsup_nhds (a : α) : Limsup (𝓝 a) = a :=
-cInf_intro (is_bounded_le_nhds a)
-  (assume a' (h : {n : α | n ≤ a'} ∈ 𝓝 a), show a ≤ a', from @mem_of_nhds α _ a _ h)
-  (assume b (hba : a < b), show ∃c (h : {n : α | n ≤ c} ∈ 𝓝 a), c < b, from
-    match dense_or_discrete a b with
-    | or.inl ⟨c, hac, hcb⟩ := ⟨c, ge_mem_nhds hac, hcb⟩
-    | or.inr ⟨_, h⟩        := ⟨a, (𝓝 a).sets_of_superset (gt_mem_nhds hba) h, hba⟩
-    end)
-
-theorem Liminf_nhds : ∀ (a : α), Liminf (𝓝 a) = a :=
-@Limsup_nhds (order_dual α) _ _ _
-
-/-- If a filter is converging, its limsup coincides with its limit. -/
-theorem Liminf_eq_of_le_nhds {f : filter α} {a : α} [ne_bot f] (h : f ≤ 𝓝 a) : f.Liminf = a :=
-have hb_ge : is_bounded (≥) f, from (is_bounded_ge_nhds a).mono h,
-have hb_le : is_bounded (≤) f, from (is_bounded_le_nhds a).mono h,
-le_antisymm
-  (calc f.Liminf ≤ f.Limsup : Liminf_le_Limsup hb_le hb_ge
-    ... ≤ (𝓝 a).Limsup :
-      Limsup_le_Limsup_of_le h hb_ge.is_cobounded_flip (is_bounded_le_nhds a)
-    ... = a : Limsup_nhds a)
-  (calc a = (𝓝 a).Liminf : (Liminf_nhds a).symm
-    ... ≤ f.Liminf :
-      Liminf_le_Liminf_of_le h (is_bounded_ge_nhds a) hb_le.is_cobounded_flip)
-
-/-- If a filter is converging, its liminf coincides with its limit. -/
-theorem Limsup_eq_of_le_nhds : ∀ {f : filter α} {a : α} [ne_bot f], f ≤ 𝓝 a → f.Limsup = a :=
-@Liminf_eq_of_le_nhds (order_dual α) _ _ _
-
-/-- If a function has a limit, then its limsup coincides with its limit. -/
-theorem filter.tendsto.limsup_eq {f : filter β} {u : β → α} {a : α} [ne_bot f]
-  (h : tendsto u f (𝓝 a)) : limsup f u = a :=
-Limsup_eq_of_le_nhds h
-
-/-- If a function has a limit, then its liminf coincides with its limit. -/
-theorem filter.tendsto.liminf_eq {f : filter β} {u : β → α} {a : α} [ne_bot f]
-  (h : tendsto u f (𝓝 a)) : liminf f u = a :=
-Liminf_eq_of_le_nhds h
-
-end conditionally_complete_linear_order
-
-section complete_linear_order
-variables [complete_linear_order α] [topological_space α] [order_topology α]
--- In complete_linear_order, the above theorems take a simpler form
-
-/-- If the liminf and the limsup of a function coincide, then the limit of the function
-exists and has the same value -/
-theorem tendsto_of_liminf_eq_limsup {f : filter β} {u : β → α} {a : α}
-  (hinf : liminf f u = a) (hsup : limsup f u = a) : tendsto u f (𝓝 a) :=
-le_nhds_of_Limsup_eq_Liminf is_bounded_le_of_top is_bounded_ge_of_bot hsup hinf
-
-/-- If a number `a` is less than or equal to the `liminf` of a function `f` at some filter
-and is greater than or equal to the `limsup` of `f`, then `f` tends to `a` along this filter. -/
-theorem tendsto_of_le_liminf_of_limsup_le {f : filter β} {u : β → α} {a : α}
-  (hinf : a ≤ liminf f u) (hsup : limsup f u ≤ a) :
-  tendsto u f (𝓝 a) :=
-if hf : f = ⊥ then hf.symm ▸ tendsto_bot
-else by haveI : ne_bot f := ⟨hf⟩; exact tendsto_of_liminf_eq_limsup
-  (le_antisymm (le_trans liminf_le_limsup hsup) hinf)
-  (le_antisymm hsup (le_trans hinf liminf_le_limsup))
-
-end complete_linear_order
-
-end liminf_limsup
-
 end order_topology
 
 /-!
@@ -3049,71 +2916,6 @@ lemma continuous_at_iff_continuous_left_right [topological_space α] [linear_ord
   continuous_at f a ↔ continuous_within_at f (Iic a) a ∧ continuous_within_at f (Ici a) a :=
 by simp only [continuous_within_at, continuous_at, ← tendsto_sup, nhds_left_sup_nhds_right]
 
-lemma continuous_on_Icc_extend_from_Ioo [topological_space α] [linear_order α] [densely_ordered α]
-  [order_topology α] [topological_space β] [regular_space β] {f : α → β} {a b : α}
-  {la lb : β} (hab : a < b) (hf : continuous_on f (Ioo a b))
-  (ha : tendsto f (𝓝[Ioi a] a) (𝓝 la)) (hb : tendsto f (𝓝[Iio b] b) (𝓝 lb)) :
-  continuous_on (extend_from (Ioo a b) f) (Icc a b) :=
-begin
-  apply continuous_on_extend_from,
-  { rw closure_Ioo hab, },
-  { intros x x_in,
-    rcases mem_Ioo_or_eq_endpoints_of_mem_Icc x_in with rfl | rfl | h,
-    { use la,
-      simpa [hab] },
-    { use lb,
-      simpa [hab] },
-    { use [f x, hf x h] } }
-end
-
-lemma eq_lim_at_left_extend_from_Ioo [topological_space α] [linear_order α] [densely_ordered α]
-  [order_topology α] [topological_space β] [t2_space β] {f : α → β} {a b : α}
-  {la : β} (hab : a < b) (ha : tendsto f (𝓝[Ioi a] a) (𝓝 la)) :
-  extend_from (Ioo a b) f a = la :=
-begin
-  apply extend_from_eq,
-  { rw closure_Ioo hab,
-    simp only [le_of_lt hab, left_mem_Icc, right_mem_Icc] },
-  { simpa [hab] }
-end
-
-lemma eq_lim_at_right_extend_from_Ioo [topological_space α] [linear_order α] [densely_ordered α]
-  [order_topology α] [topological_space β] [t2_space β] {f : α → β} {a b : α}
-  {lb : β} (hab : a < b) (hb : tendsto f (𝓝[Iio b] b) (𝓝 lb)) :
-  extend_from (Ioo a b) f b = lb :=
-begin
-  apply extend_from_eq,
-  { rw closure_Ioo hab,
-    simp only [le_of_lt hab, left_mem_Icc, right_mem_Icc] },
-  { simpa [hab] }
-end
-
-lemma continuous_on_Ico_extend_from_Ioo [topological_space α]
-  [linear_order α] [densely_ordered α] [order_topology α] [topological_space β]
-  [regular_space β] {f : α → β} {a b : α} {la : β} (hab : a < b) (hf : continuous_on f (Ioo a b))
-  (ha : tendsto f (𝓝[Ioi a] a) (𝓝 la)) :
-  continuous_on (extend_from (Ioo a b) f) (Ico a b) :=
-begin
-  apply continuous_on_extend_from,
-  { rw [closure_Ioo hab], exact Ico_subset_Icc_self, },
-  { intros x x_in,
-    rcases mem_Ioo_or_eq_left_of_mem_Ico x_in with rfl | h,
-    { use la,
-      simpa [hab] },
-    { use [f x, hf x h] } }
-end
-
-lemma continuous_on_Ioc_extend_from_Ioo [topological_space α]
-  [linear_order α] [densely_ordered α] [order_topology α] [topological_space β]
-  [regular_space β] {f : α → β} {a b : α} {lb : β} (hab : a < b) (hf : continuous_on f (Ioo a b))
-  (hb : tendsto f (𝓝[Iio b] b) (𝓝 lb)) :
-  continuous_on (extend_from (Ioo a b) f) (Ioc a b) :=
-begin
-  have := @continuous_on_Ico_extend_from_Ioo (order_dual α) _ _ _ _ _ _ _ f _ _ _ hab,
-  erw [dual_Ico, dual_Ioi, dual_Ioo] at this,
-  exact this hf hb
-end
-
 lemma continuous_within_at_Ioi_iff_Ici {α β : Type*} [topological_space α] [partial_order α]
   [topological_space β] {a : α} {f : α → β} :
   continuous_within_at f (Ioi a) a ↔ continuous_within_at f (Ici a) a :=

src/topology/algebra/ordered/extend_from.lean

@@ -0,0 +1,82 @@
+/-
+Copyright (c) 2017 Johannes Hölzl. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johannes Hölzl, Mario Carneiro, Yury Kudryashov
+-/
+import topology.algebra.ordered.basic
+import topology.extend_from
+
+/-!
+# Lemmas about `extend_from` in an order topology.
+-/
+
+open filter set topological_space
+open_locale topological_space classical
+
+universes u v
+variables {α : Type u} {β : Type v}
+
+lemma continuous_on_Icc_extend_from_Ioo [topological_space α] [linear_order α] [densely_ordered α]
+  [order_topology α] [topological_space β] [regular_space β] {f : α → β} {a b : α}
+  {la lb : β} (hab : a < b) (hf : continuous_on f (Ioo a b))
+  (ha : tendsto f (𝓝[Ioi a] a) (𝓝 la)) (hb : tendsto f (𝓝[Iio b] b) (𝓝 lb)) :
+  continuous_on (extend_from (Ioo a b) f) (Icc a b) :=
+begin
+  apply continuous_on_extend_from,
+  { rw closure_Ioo hab, },
+  { intros x x_in,
+    rcases mem_Ioo_or_eq_endpoints_of_mem_Icc x_in with rfl | rfl | h,
+    { use la,
+      simpa [hab] },
+    { use lb,
+      simpa [hab] },
+    { use [f x, hf x h] } }
+end
+
+lemma eq_lim_at_left_extend_from_Ioo [topological_space α] [linear_order α] [densely_ordered α]
+  [order_topology α] [topological_space β] [t2_space β] {f : α → β} {a b : α}
+  {la : β} (hab : a < b) (ha : tendsto f (𝓝[Ioi a] a) (𝓝 la)) :
+  extend_from (Ioo a b) f a = la :=
+begin
+  apply extend_from_eq,
+  { rw closure_Ioo hab,
+    simp only [le_of_lt hab, left_mem_Icc, right_mem_Icc] },
+  { simpa [hab] }
+end
+
+lemma eq_lim_at_right_extend_from_Ioo [topological_space α] [linear_order α] [densely_ordered α]
+  [order_topology α] [topological_space β] [t2_space β] {f : α → β} {a b : α}
+  {lb : β} (hab : a < b) (hb : tendsto f (𝓝[Iio b] b) (𝓝 lb)) :
+  extend_from (Ioo a b) f b = lb :=
+begin
+  apply extend_from_eq,
+  { rw closure_Ioo hab,
+    simp only [le_of_lt hab, left_mem_Icc, right_mem_Icc] },
+  { simpa [hab] }
+end
+
+lemma continuous_on_Ico_extend_from_Ioo [topological_space α]
+  [linear_order α] [densely_ordered α] [order_topology α] [topological_space β]
+  [regular_space β] {f : α → β} {a b : α} {la : β} (hab : a < b) (hf : continuous_on f (Ioo a b))
+  (ha : tendsto f (𝓝[Ioi a] a) (𝓝 la)) :
+  continuous_on (extend_from (Ioo a b) f) (Ico a b) :=
+begin
+  apply continuous_on_extend_from,
+  { rw [closure_Ioo hab], exact Ico_subset_Icc_self, },
+  { intros x x_in,
+    rcases mem_Ioo_or_eq_left_of_mem_Ico x_in with rfl | h,
+    { use la,
+      simpa [hab] },
+    { use [f x, hf x h] } }
+end
+
+lemma continuous_on_Ioc_extend_from_Ioo [topological_space α]
+  [linear_order α] [densely_ordered α] [order_topology α] [topological_space β]
+  [regular_space β] {f : α → β} {a b : α} {lb : β} (hab : a < b) (hf : continuous_on f (Ioo a b))
+  (hb : tendsto f (𝓝[Iio b] b) (𝓝 lb)) :
+  continuous_on (extend_from (Ioo a b) f) (Ioc a b) :=
+begin
+  have := @continuous_on_Ico_extend_from_Ioo (order_dual α) _ _ _ _ _ _ _ f _ _ _ hab,
+  erw [dual_Ico, dual_Ioi, dual_Ioo] at this,
+  exact this hf hb
+end