refactor(Topology/Order/Basic): split up large file (#11992)

This splits up the file `Mathlib/Topology/Order/Basic.lean` (currently > 2000 lines) into several smaller files.

Mathlib.lean

@@ -3993,17 +3993,21 @@ 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.DenselyOrdered
 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.IsLUB
 import Mathlib.Topology.Order.Lattice
 import Mathlib.Topology.Order.LeftRight
 import Mathlib.Topology.Order.LeftRightLim
+import Mathlib.Topology.Order.LeftRightNhds
 import Mathlib.Topology.Order.LocalExtr
 import Mathlib.Topology.Order.LowerUpperTopology
+import Mathlib.Topology.Order.Monotone
 import Mathlib.Topology.Order.MonotoneContinuity
 import Mathlib.Topology.Order.MonotoneConvergence
 import Mathlib.Topology.Order.NhdsSet

Mathlib/Algebra/ContinuedFractions/Computation/ApproximationCorollaries.lean

@@ -7,7 +7,7 @@ import Mathlib.Algebra.ContinuedFractions.Computation.Approximations
 import Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
 import Mathlib.Algebra.Order.Archimedean
 import Mathlib.Tactic.GCongr
-import Mathlib.Topology.Order.Basic
+import Mathlib.Topology.Order.LeftRightNhds
 
 #align_import algebra.continued_fractions.computation.approximation_corollaries from "leanprover-community/mathlib"@"f0c8bf9245297a541f468be517f1bde6195105e9"
 

Mathlib/Analysis/Convex/Strict.lean

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
 import Mathlib.Analysis.Convex.Basic
-import Mathlib.Topology.Order.Basic
 import Mathlib.Topology.Algebra.Group.Basic
+import Mathlib.Topology.Order.Basic
 
 #align_import analysis.convex.strict from "leanprover-community/mathlib"@"84dc0bd6619acaea625086d6f53cb35cdd554219"
 

Mathlib/SetTheory/Ordinal/Topology.lean

@@ -5,7 +5,7 @@ Authors: Violeta Hernández Palacios
 -/
 import Mathlib.SetTheory.Ordinal.Arithmetic
 import Mathlib.Tactic.TFAE
-import Mathlib.Topology.Order.Basic
+import Mathlib.Topology.Order.Monotone
 
 #align_import set_theory.ordinal.topology from "leanprover-community/mathlib"@"740acc0e6f9adf4423f92a485d0456fc271482da"
 

Mathlib/Topology/Algebra/Order/Archimedean.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.Order.Basic
 import Mathlib.GroupTheory.Archimedean
+import Mathlib.Topology.Order.Basic
 
 #align_import topology.algebra.order.archimedean from "leanprover-community/mathlib"@"4c19a16e4b705bf135cf9a80ac18fcc99c438514"
 

Mathlib/Topology/Algebra/Order/Compact.lean

@@ -6,6 +6,7 @@ Authors: Patrick Massot, Yury Kudryashov
 import Mathlib.Topology.Order.LocalExtr
 import Mathlib.Topology.Order.IntermediateValue
 import Mathlib.Topology.Support
+import Mathlib.Topology.Order.IsLUB
 
 #align_import topology.algebra.order.compact from "leanprover-community/mathlib"@"3efd324a3a31eaa40c9d5bfc669c4fafee5f9423"
 

Mathlib/Topology/Algebra/Order/Field.lean

@@ -6,6 +6,7 @@ Authors: Benjamin Davidson, Devon Tuma, Eric Rodriguez, Oliver Nash
 import Mathlib.Topology.Algebra.Order.Group
 import Mathlib.Topology.Algebra.Field
 import Mathlib.Data.Set.Pointwise.Interval
+import Mathlib.Topology.Order.LeftRightNhds
 
 #align_import topology.algebra.order.field from "leanprover-community/mathlib"@"9a59dcb7a2d06bf55da57b9030169219980660cd"
 

Mathlib/Topology/Algebra/Order/Floor.lean

@@ -5,6 +5,7 @@ Authors: Anatole Dedecker
 -/
 import Mathlib.Algebra.Order.Floor
 import Mathlib.Topology.Algebra.Order.Group
+import Mathlib.Topology.Order.Basic
 
 #align_import topology.algebra.order.floor from "leanprover-community/mathlib"@"84dc0bd6619acaea625086d6f53cb35cdd554219"
 

Mathlib/Topology/Algebra/Order/Group.lean

@@ -3,8 +3,8 @@ Copyright (c) 2020 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.Algebra.Group.Basic
+import Mathlib.Topology.Order.LeftRightNhds
 
 #align_import topology.algebra.order.group from "leanprover-community/mathlib"@"84dc0bd6619acaea625086d6f53cb35cdd554219"
 

Mathlib/Topology/Algebra/Order/LiminfLimsup.lean

@@ -10,8 +10,8 @@ import Mathlib.Order.LiminfLimsup
 import Mathlib.Order.Filter.Archimedean
 import Mathlib.Order.Filter.CountableInter
 import Mathlib.Topology.Algebra.Group.Basic
-import Mathlib.Topology.Order.Basic
 import Mathlib.Data.Set.Lattice
+import Mathlib.Topology.Order.Monotone
 
 #align_import topology.algebra.order.liminf_limsup from "leanprover-community/mathlib"@"ce64cd319bb6b3e82f31c2d38e79080d377be451"
 

Mathlib/Topology/FiberBundle/Basic.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel, Floris van Doorn, Heather Macbeth
 -/
 import Mathlib.Topology.FiberBundle.Trivialization
+import Mathlib.Topology.Order.LeftRightNhds
 
 #align_import topology.fiber_bundle.basic from "leanprover-community/mathlib"@"e473c3198bb41f68560cab68a0529c854b618833"
 

Mathlib/Topology/MetricSpace/PseudoMetric.lean

@@ -7,6 +7,7 @@ import Mathlib.Topology.Algebra.Order.Compact
 import Mathlib.Topology.EMetricSpace.Basic
 import Mathlib.Topology.Bornology.Constructions
 import Mathlib.Data.Set.Pointwise.Interval
+import Mathlib.Topology.Order.DenselyOrdered
 
 /-!
 ## Pseudo-metric spaces