move(Topology/Order): Move anything that doesn't concern algebra (#11610

)

Move files from `Topology.Algebra.Order` to `Topology.Order` when they do not contain any algebra. Also move `Topology.LocalExtr` to `Topology.Order.LocalExtr`.

According to git, the moves are:

* `Mathlib/Topology/{Algebra => }/Order/ExtendFrom.lean`
* `Mathlib/Topology/{Algebra => }/Order/ExtrClosure.lean`
* `Mathlib/Topology/{Algebra => }/Order/Filter.lean`
* `Mathlib/Topology/{Algebra => }/Order/IntermediateValue.lean`
* `Mathlib/Topology/{Algebra => }/Order/LeftRight.lean`
* `Mathlib/Topology/{Algebra => }/Order/LeftRightLim.lean`
* `Mathlib/Topology/{Algebra => }/Order/MonotoneContinuity.lean`
* `Mathlib/Topology/{Algebra => }/Order/MonotoneConvergence.lean`
* `Mathlib/Topology/{Algebra => }/Order/ProjIcc.lean`
* `Mathlib/Topology/{Algebra => }/Order/T5.lean`
* `Mathlib/Topology/{ => Order}/LocalExtr.lean`

Mathlib.lean

@@ -3756,21 +3756,11 @@ import Mathlib.Topology.Algebra.Nonarchimedean.Basic
 import Mathlib.Topology.Algebra.OpenSubgroup
 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.Field
-import Mathlib.Topology.Algebra.Order.Filter
 import Mathlib.Topology.Algebra.Order.Floor
 import Mathlib.Topology.Algebra.Order.Group
-import Mathlib.Topology.Algebra.Order.IntermediateValue
-import Mathlib.Topology.Algebra.Order.LeftRight
-import Mathlib.Topology.Algebra.Order.LeftRightLim
 import Mathlib.Topology.Algebra.Order.LiminfLimsup
-import Mathlib.Topology.Algebra.Order.MonotoneContinuity
-import Mathlib.Topology.Algebra.Order.MonotoneConvergence
-import Mathlib.Topology.Algebra.Order.ProjIcc
 import Mathlib.Topology.Algebra.Order.Rolle
-import Mathlib.Topology.Algebra.Order.T5
 import Mathlib.Topology.Algebra.Order.UpperLower
 import Mathlib.Topology.Algebra.Polynomial
 import Mathlib.Topology.Algebra.PontryaginDual
@@ -3922,7 +3912,6 @@ import Mathlib.Topology.Irreducible
 import Mathlib.Topology.IsLocalHomeomorph
 import Mathlib.Topology.List
 import Mathlib.Topology.LocalAtTarget
-import Mathlib.Topology.LocalExtr
 import Mathlib.Topology.LocallyConstant.Algebra
 import Mathlib.Topology.LocallyConstant.Basic
 import Mathlib.Topology.LocallyFinite
@@ -3974,15 +3963,26 @@ import Mathlib.Topology.Order.Basic
 import Mathlib.Topology.Order.Bounded
 import Mathlib.Topology.Order.Category.AlexDisc
 import Mathlib.Topology.Order.Category.FrameAdjunction
+import Mathlib.Topology.Order.ExtendFrom
+import Mathlib.Topology.Order.ExtrClosure
+import Mathlib.Topology.Order.Filter
 import Mathlib.Topology.Order.Hom.Basic
 import Mathlib.Topology.Order.Hom.Esakia
+import Mathlib.Topology.Order.IntermediateValue
 import Mathlib.Topology.Order.Lattice
+import Mathlib.Topology.Order.LeftRight
+import Mathlib.Topology.Order.LeftRightLim
+import Mathlib.Topology.Order.LocalExtr
 import Mathlib.Topology.Order.LowerUpperTopology
+import Mathlib.Topology.Order.MonotoneContinuity
+import Mathlib.Topology.Order.MonotoneConvergence
 import Mathlib.Topology.Order.NhdsSet
 import Mathlib.Topology.Order.OrderClosed
 import Mathlib.Topology.Order.PartialSups
 import Mathlib.Topology.Order.Priestley
+import Mathlib.Topology.Order.ProjIcc
 import Mathlib.Topology.Order.ScottTopology
+import Mathlib.Topology.Order.T5
 import Mathlib.Topology.Order.UpperLowerSetTopology
 import Mathlib.Topology.Partial
 import Mathlib.Topology.PartialHomeomorph

Mathlib/Analysis/BoxIntegral/Box/Basic.lean

@@ -4,9 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
 import Mathlib.Data.Set.Intervals.Monotone
-import Mathlib.Topology.Algebra.Order.MonotoneConvergence
-import Mathlib.Topology.MetricSpace.Bounded
 import Mathlib.Topology.MetricSpace.Basic
+import Mathlib.Topology.MetricSpace.Bounded
+import Mathlib.Topology.Order.MonotoneConvergence
 
 #align_import analysis.box_integral.box.basic from "leanprover-community/mathlib"@"f2ce6086713c78a7f880485f7917ea547a215982"
 /-!

Mathlib/Analysis/Complex/AbsMax.lean

@@ -6,7 +6,7 @@ Authors: Yury G. Kudryashov
 import Mathlib.Analysis.Complex.CauchyIntegral
 import Mathlib.Analysis.NormedSpace.Completion
 import Mathlib.Analysis.NormedSpace.Extr
-import Mathlib.Topology.Algebra.Order.ExtrClosure
+import Mathlib.Topology.Order.ExtrClosure
 
 #align_import analysis.complex.abs_max from "leanprover-community/mathlib"@"f2ce6086713c78a7f880485f7917ea547a215982"
 

Mathlib/Analysis/NormedSpace/Extr.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
 import Mathlib.Analysis.NormedSpace.Ray
-import Mathlib.Topology.LocalExtr
+import Mathlib.Topology.Order.LocalExtr
 
 #align_import analysis.normed_space.extr from "leanprover-community/mathlib"@"17ef379e997badd73e5eabb4d38f11919ab3c4b3"
 

Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Abhimanyu Pallavi Sudhir, Jean Lo, Calle Sönne, Benjamin Davidson
 -/
 import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
-import Mathlib.Topology.Algebra.Order.ProjIcc
+import Mathlib.Topology.Order.ProjIcc
 
 #align_import analysis.special_functions.trigonometric.inverse from "leanprover-community/mathlib"@"f2ce6086713c78a7f880485f7917ea547a215982"
 

Mathlib/Data/Real/Sqrt.lean

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Floris van Doorn, Yury Kudryashov
 -/
 import Mathlib.Algebra.Star.Order
-import Mathlib.Topology.Algebra.Order.MonotoneContinuity
 import Mathlib.Topology.Instances.NNReal
+import Mathlib.Topology.Order.MonotoneContinuity
 
 #align_import data.real.sqrt from "leanprover-community/mathlib"@"31c24aa72e7b3e5ed97a8412470e904f82b81004"
 

Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean

@@ -8,7 +8,7 @@ import Mathlib.Analysis.SpecificLimits.Basic
 import Mathlib.Order.Iterate
 import Mathlib.Order.SemiconjSup
 import Mathlib.Tactic.Monotonicity
-import Mathlib.Topology.Algebra.Order.MonotoneContinuity
+import Mathlib.Topology.Order.MonotoneContinuity
 
 #align_import dynamics.circle.rotation_number.translation_number from "leanprover-community/mathlib"@"f2ce6086713c78a7f880485f7917ea547a215982"
 

Mathlib/MeasureTheory/Measure/Stieltjes.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Yury Kudryashov, Sébastien Gouëzel
 -/
 import Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
-import Mathlib.Topology.Algebra.Order.LeftRightLim
+import Mathlib.Topology.Order.LeftRightLim
 
 #align_import measure_theory.measure.stieltjes from "leanprover-community/mathlib"@"20d5763051978e9bc6428578ed070445df6a18b3"
 

Mathlib/Topology/Algebra/Field.lean

@@ -6,7 +6,7 @@ Authors: Patrick Massot, Scott Morrison
 import Mathlib.Algebra.GroupPower.Ring
 import Mathlib.Topology.Algebra.Ring.Basic
 import Mathlib.Topology.Algebra.GroupWithZero
-import Mathlib.Topology.LocalExtr
+import Mathlib.Topology.Order.LocalExtr
 import Mathlib.FieldTheory.Subfield
 
 #align_import topology.algebra.field from "leanprover-community/mathlib"@"c10e724be91096453ee3db13862b9fb9a992fef2"

Mathlib/Topology/Algebra/InfiniteSum/Order.lean

@@ -6,7 +6,7 @@ Authors: Johannes Hölzl
 import Mathlib.Algebra.Order.Archimedean
 import Mathlib.Topology.Algebra.InfiniteSum.NatInt
 import Mathlib.Topology.Algebra.Order.Field
-import Mathlib.Topology.Algebra.Order.MonotoneConvergence
+import Mathlib.Topology.Order.MonotoneConvergence
 
 #align_import topology.algebra.infinite_sum.order from "leanprover-community/mathlib"@"32253a1a1071173b33dc7d6a218cf722c6feb514"
 

Mathlib/Topology/Algebra/Order/Compact.lean

@@ -3,8 +3,8 @@ Copyright (c) 2021 Patrick Massot. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Patrick Massot, Yury Kudryashov
 -/
-import Mathlib.Topology.Algebra.Order.IntermediateValue
-import Mathlib.Topology.LocalExtr
+import Mathlib.Topology.Order.LocalExtr
+import Mathlib.Topology.Order.IntermediateValue
 import Mathlib.Topology.Support
 
 #align_import topology.algebra.order.compact from "leanprover-community/mathlib"@"3efd324a3a31eaa40c9d5bfc669c4fafee5f9423"

Mathlib/Topology/Algebra/Order/Rolle.lean

@@ -3,10 +3,10 @@ Copyright (c) 2019 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
-import Mathlib.Topology.Algebra.Order.ExtendFrom
+import Mathlib.Topology.Order.ExtendFrom
 import Mathlib.Topology.Algebra.Order.Compact
-import Mathlib.Topology.Algebra.Order.T5
-import Mathlib.Topology.LocalExtr
+import Mathlib.Topology.Order.LocalExtr
+import Mathlib.Topology.Order.T5
 
 #align_import analysis.calculus.local_extr from "leanprover-community/mathlib"@"3bce8d800a6f2b8f63fe1e588fd76a9ff4adcebe"
 

Mathlib/Topology/Connected/PathConnected.lean

@@ -3,7 +3,7 @@ Copyright (c) 2020 Patrick Massot. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Patrick Massot
 -/
-import Mathlib.Topology.Algebra.Order.ProjIcc
+import Mathlib.Topology.Order.ProjIcc
 import Mathlib.Topology.CompactOpen
 import Mathlib.Topology.UnitInterval
 

Mathlib/Topology/ContinuousFunction/Ordered.lean

@@ -3,9 +3,9 @@ Copyright © 2021 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison, Shing Tak Lam
 -/
-import Mathlib.Topology.Algebra.Order.ProjIcc
 import Mathlib.Topology.ContinuousFunction.Basic
 import Mathlib.Topology.Order.Lattice
+import Mathlib.Topology.Order.ProjIcc
 
 #align_import topology.continuous_function.ordered from "leanprover-community/mathlib"@"84dc0bd6619acaea625086d6f53cb35cdd554219"
 

Mathlib/Topology/Homotopy/Basic.lean

@@ -3,7 +3,7 @@ Copyright (c) 2021 Shing Tak Lam. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Shing Tak Lam
 -/
-import Mathlib.Topology.Algebra.Order.ProjIcc
+import Mathlib.Topology.Order.ProjIcc
 import Mathlib.Topology.ContinuousFunction.Ordered
 import Mathlib.Topology.CompactOpen
 import Mathlib.Topology.UnitInterval

Mathlib/Topology/Instances/ENNReal.lean

@@ -3,13 +3,13 @@ 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
 -/
-import Mathlib.Topology.Instances.NNReal
-import Mathlib.Topology.Algebra.Order.MonotoneContinuity
+import Mathlib.Topology.Order.MonotoneContinuity
 import Mathlib.Topology.Algebra.InfiniteSum.Real
 import Mathlib.Topology.Algebra.Order.LiminfLimsup
-import Mathlib.Topology.Algebra.Order.T5
+import Mathlib.Topology.Instances.NNReal
 import Mathlib.Topology.EMetricSpace.Lipschitz
 import Mathlib.Topology.Metrizable.Basic
+import Mathlib.Topology.Order.T5
 
 #align_import topology.instances.ennreal from "leanprover-community/mathlib"@"ec4b2eeb50364487f80421c0b4c41328a611f30d"
 

Mathlib/Topology/Instances/EReal.lean

@@ -5,8 +5,8 @@ Authors: Sébastien Gouëzel
 -/
 import Mathlib.Data.Rat.Encodable
 import Mathlib.Data.Real.EReal
-import Mathlib.Topology.Algebra.Order.MonotoneContinuity
 import Mathlib.Topology.Instances.ENNReal
+import Mathlib.Topology.Order.MonotoneContinuity
 
 #align_import topology.instances.ereal from "leanprover-community/mathlib"@"f2ce6086713c78a7f880485f7917ea547a215982"
 

Mathlib/Topology/Order/Basic.lean

@@ -8,8 +8,8 @@ import Mathlib.Data.Set.Pointwise.Basic
 import Mathlib.Order.Filter.Interval
 import Mathlib.Tactic.TFAE
 import Mathlib.Tactic.NormNum
+import Mathlib.Topology.Order.LeftRight
 import Mathlib.Topology.Order.OrderClosed
-import Mathlib.Topology.Algebra.Order.LeftRight
 
 #align_import topology.order.basic from "leanprover-community/mathlib"@"3efd324a3a31eaa40c9d5bfc669c4fafee5f9423"
 

Mathlib/Topology/Algebra/Order/ExtendFrom.lean → Mathlib/Topology/Order/ExtendFrom.lean

@@ -3,8 +3,8 @@ 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 Mathlib.Topology.Order.Basic
 import Mathlib.Topology.ExtendFrom
+import Mathlib.Topology.Order.Basic
 
 #align_import topology.algebra.order.extend_from from "leanprover-community/mathlib"@"0a0ec35061ed9960bf0e7ffb0335f44447b58977"
 

Mathlib/Topology/Algebra/Order/ExtrClosure.lean → Mathlib/Topology/Order/ExtrClosure.lean

@@ -3,8 +3,8 @@ Copyright (c) 2022 Yury G. Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury G. Kudryashov
 -/
-import Mathlib.Topology.LocalExtr
 import Mathlib.Topology.Order.OrderClosed
+import Mathlib.Topology.Order.LocalExtr
 
 #align_import topology.algebra.order.extr_closure from "leanprover-community/mathlib"@"4c19a16e4b705bf135cf9a80ac18fcc99c438514"
 

Mathlib/Topology/Algebra/Order/Filter.lean → Mathlib/Topology/Order/Filter.lean

@@ -3,8 +3,8 @@ Copyright (c) 2022 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
-import Mathlib.Topology.Order.Basic
 import Mathlib.Topology.Filter
+import Mathlib.Topology.Order.Basic
 
 #align_import topology.algebra.order.filter from "leanprover-community/mathlib"@"98e83c3d541c77cdb7da20d79611a780ff8e7d90"
 

Mathlib/Topology/Algebra/Order/LeftRightLim.lean → Mathlib/Topology/Order/LeftRightLim.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 -/
 import Mathlib.Topology.Order.Basic
-import Mathlib.Topology.Algebra.Order.LeftRight
+import Mathlib.Topology.Order.LeftRight
 
 #align_import topology.algebra.order.left_right_lim from "leanprover-community/mathlib"@"0a0ec35061ed9960bf0e7ffb0335f44447b58977"
 

Mathlib/Topology/LocalExtr.lean → Mathlib/Topology/Order/LocalExtr.lean

@@ -3,9 +3,9 @@ Copyright (c) 2019 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
+import Mathlib.Algebra.Group.Defs
 import Mathlib.Order.Filter.Extr
 import Mathlib.Topology.ContinuousOn
-import Mathlib.Algebra.Group.Defs
 
 #align_import topology.local_extr from "leanprover-community/mathlib"@"bcfa726826abd57587355b4b5b7e78ad6527b7e4"
 
@@ -629,4 +629,3 @@ theorem Filter.EventuallyEq.isLocalExtr_iff {f g : α → β} {a : α} (heq : f
 #align filter.eventually_eq.is_local_extr_iff Filter.EventuallyEq.isLocalExtr_iff
 
 end Eventually
-

Mathlib/Topology/Algebra/Order/MonotoneContinuity.lean → Mathlib/Topology/Order/MonotoneContinuity.lean

@@ -3,8 +3,8 @@ Copyright (c) 2021 Yury G. Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury G. Kudryashov, Heather Macbeth
 -/
-import Mathlib.Topology.Order.Basic
 import Mathlib.Topology.Homeomorph
+import Mathlib.Topology.Order.Basic
 
 #align_import topology.algebra.order.monotone_continuity from "leanprover-community/mathlib"@"4c19a16e4b705bf135cf9a80ac18fcc99c438514"
 

Mathlib/Topology/Algebra/Order/T5.lean → Mathlib/Topology/Order/T5.lean

@@ -3,8 +3,8 @@ Copyright (c) 2022 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
-import Mathlib.Topology.Order.Basic
 import Mathlib.Data.Set.Intervals.OrdConnectedComponent
+import Mathlib.Topology.Order.Basic
 
 #align_import topology.algebra.order.t5 from "leanprover-community/mathlib"@"4c19a16e4b705bf135cf9a80ac18fcc99c438514"
 

Mathlib/Topology/TietzeExtension.lean

@@ -5,7 +5,7 @@ Authors: Yury G. Kudryashov
 -/
 import Mathlib.Analysis.SpecificLimits.Basic
 import Mathlib.Data.Set.Intervals.IsoIoo
-import Mathlib.Topology.Algebra.Order.MonotoneContinuity
+import Mathlib.Topology.Order.MonotoneContinuity
 import Mathlib.Topology.UrysohnsBounded
 
 #align_import topology.tietze_extension from "leanprover-community/mathlib"@"f2ce6086713c78a7f880485f7917ea547a215982"