From cd9902cc6977109300779405515040a4dbcaf2fa Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Sat, 23 Mar 2024 17:33:58 +0000 Subject: [PATCH] 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 | 22 +++++++++---------- Mathlib/Analysis/BoxIntegral/Box/Basic.lean | 4 ++-- Mathlib/Analysis/Complex/AbsMax.lean | 2 +- Mathlib/Analysis/NormedSpace/Extr.lean | 2 +- .../Trigonometric/Inverse.lean | 2 +- Mathlib/Data/Real/Sqrt.lean | 2 +- .../RotationNumber/TranslationNumber.lean | 2 +- Mathlib/MeasureTheory/Measure/Stieltjes.lean | 2 +- Mathlib/Topology/Algebra/Field.lean | 2 +- .../Topology/Algebra/InfiniteSum/Order.lean | 2 +- Mathlib/Topology/Algebra/Order/Compact.lean | 4 ++-- Mathlib/Topology/Algebra/Order/Rolle.lean | 6 ++--- Mathlib/Topology/Connected/PathConnected.lean | 2 +- .../Topology/ContinuousFunction/Ordered.lean | 2 +- Mathlib/Topology/Homotopy/Basic.lean | 2 +- Mathlib/Topology/Instances/ENNReal.lean | 6 ++--- Mathlib/Topology/Instances/EReal.lean | 2 +- Mathlib/Topology/Order/Basic.lean | 2 +- .../{Algebra => }/Order/ExtendFrom.lean | 2 +- .../{Algebra => }/Order/ExtrClosure.lean | 2 +- .../Topology/{Algebra => }/Order/Filter.lean | 2 +- .../Order/IntermediateValue.lean | 0 .../{Algebra => }/Order/LeftRight.lean | 0 .../{Algebra => }/Order/LeftRightLim.lean | 2 +- Mathlib/Topology/{ => Order}/LocalExtr.lean | 3 +-- .../Order/MonotoneContinuity.lean | 2 +- .../Order/MonotoneConvergence.lean | 0 .../Topology/{Algebra => }/Order/ProjIcc.lean | 0 Mathlib/Topology/{Algebra => }/Order/T5.lean | 2 +- Mathlib/Topology/TietzeExtension.lean | 2 +- 30 files changed, 42 insertions(+), 43 deletions(-) rename Mathlib/Topology/{Algebra => }/Order/ExtendFrom.lean (100%) rename Mathlib/Topology/{Algebra => }/Order/ExtrClosure.lean (98%) rename Mathlib/Topology/{Algebra => }/Order/Filter.lean (100%) rename Mathlib/Topology/{Algebra => }/Order/IntermediateValue.lean (100%) rename Mathlib/Topology/{Algebra => }/Order/LeftRight.lean (100%) rename Mathlib/Topology/{Algebra => }/Order/LeftRightLim.lean (99%) rename Mathlib/Topology/{ => Order}/LocalExtr.lean (99%) rename Mathlib/Topology/{Algebra => }/Order/MonotoneContinuity.lean (100%) rename Mathlib/Topology/{Algebra => }/Order/MonotoneConvergence.lean (100%) rename Mathlib/Topology/{Algebra => }/Order/ProjIcc.lean (100%) rename Mathlib/Topology/{Algebra => }/Order/T5.lean (100%) diff --git a/Mathlib.lean b/Mathlib.lean index 37528c685d812..16da2fea23772 100644 --- a/Mathlib.lean +++ b/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 diff --git a/Mathlib/Analysis/BoxIntegral/Box/Basic.lean b/Mathlib/Analysis/BoxIntegral/Box/Basic.lean index 47c188c543042..d743a4f362f75 100644 --- a/Mathlib/Analysis/BoxIntegral/Box/Basic.lean +++ b/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" /-! diff --git a/Mathlib/Analysis/Complex/AbsMax.lean b/Mathlib/Analysis/Complex/AbsMax.lean index 8063175a3faf0..c6e06d63e1412 100644 --- a/Mathlib/Analysis/Complex/AbsMax.lean +++ b/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" diff --git a/Mathlib/Analysis/NormedSpace/Extr.lean b/Mathlib/Analysis/NormedSpace/Extr.lean index b503e4571bcfe..2ed29e7b477d3 100644 --- a/Mathlib/Analysis/NormedSpace/Extr.lean +++ b/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" diff --git a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean index 3635fd9e40271..7c0ed2398a658 100644 --- a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean +++ b/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" diff --git a/Mathlib/Data/Real/Sqrt.lean b/Mathlib/Data/Real/Sqrt.lean index 28d87ea8e22f8..c089639641d1c 100644 --- a/Mathlib/Data/Real/Sqrt.lean +++ b/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" diff --git a/Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean b/Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean index d3449d2afa5a1..c88d09cce8686 100644 --- a/Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean +++ b/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" diff --git a/Mathlib/MeasureTheory/Measure/Stieltjes.lean b/Mathlib/MeasureTheory/Measure/Stieltjes.lean index 412e06b6acd8f..cebe82203e469 100644 --- a/Mathlib/MeasureTheory/Measure/Stieltjes.lean +++ b/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" diff --git a/Mathlib/Topology/Algebra/Field.lean b/Mathlib/Topology/Algebra/Field.lean index 9342d60dfccaa..635c9f2db5ee0 100644 --- a/Mathlib/Topology/Algebra/Field.lean +++ b/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" diff --git a/Mathlib/Topology/Algebra/InfiniteSum/Order.lean b/Mathlib/Topology/Algebra/InfiniteSum/Order.lean index 8e0bb0f02c379..b9e6dc4eb25e9 100644 --- a/Mathlib/Topology/Algebra/InfiniteSum/Order.lean +++ b/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" diff --git a/Mathlib/Topology/Algebra/Order/Compact.lean b/Mathlib/Topology/Algebra/Order/Compact.lean index dad8ea79ad243..2936119b76ad7 100644 --- a/Mathlib/Topology/Algebra/Order/Compact.lean +++ b/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" diff --git a/Mathlib/Topology/Algebra/Order/Rolle.lean b/Mathlib/Topology/Algebra/Order/Rolle.lean index a0fa83c2c7d47..4e304d734ef42 100644 --- a/Mathlib/Topology/Algebra/Order/Rolle.lean +++ b/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" diff --git a/Mathlib/Topology/Connected/PathConnected.lean b/Mathlib/Topology/Connected/PathConnected.lean index 366159360bdb3..c9780114ac9b0 100644 --- a/Mathlib/Topology/Connected/PathConnected.lean +++ b/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 diff --git a/Mathlib/Topology/ContinuousFunction/Ordered.lean b/Mathlib/Topology/ContinuousFunction/Ordered.lean index b5c705b37b99d..7239273ff72c1 100644 --- a/Mathlib/Topology/ContinuousFunction/Ordered.lean +++ b/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" diff --git a/Mathlib/Topology/Homotopy/Basic.lean b/Mathlib/Topology/Homotopy/Basic.lean index 5a80e6171123b..db19acd975413 100644 --- a/Mathlib/Topology/Homotopy/Basic.lean +++ b/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 diff --git a/Mathlib/Topology/Instances/ENNReal.lean b/Mathlib/Topology/Instances/ENNReal.lean index 98b019318157e..ec26bfd0658be 100644 --- a/Mathlib/Topology/Instances/ENNReal.lean +++ b/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" diff --git a/Mathlib/Topology/Instances/EReal.lean b/Mathlib/Topology/Instances/EReal.lean index 907f8a06a9848..adfa125d6d87d 100644 --- a/Mathlib/Topology/Instances/EReal.lean +++ b/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" diff --git a/Mathlib/Topology/Order/Basic.lean b/Mathlib/Topology/Order/Basic.lean index 1c7f52d552a53..8e3a879e08762 100644 --- a/Mathlib/Topology/Order/Basic.lean +++ b/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" diff --git a/Mathlib/Topology/Algebra/Order/ExtendFrom.lean b/Mathlib/Topology/Order/ExtendFrom.lean similarity index 100% rename from Mathlib/Topology/Algebra/Order/ExtendFrom.lean rename to Mathlib/Topology/Order/ExtendFrom.lean index a1b09fc49ccc1..0104fcf1f1262 100644 --- a/Mathlib/Topology/Algebra/Order/ExtendFrom.lean +++ b/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" diff --git a/Mathlib/Topology/Algebra/Order/ExtrClosure.lean b/Mathlib/Topology/Order/ExtrClosure.lean similarity index 98% rename from Mathlib/Topology/Algebra/Order/ExtrClosure.lean rename to Mathlib/Topology/Order/ExtrClosure.lean index 118f8c492360e..eebc5aa3b5dbf 100644 --- a/Mathlib/Topology/Algebra/Order/ExtrClosure.lean +++ b/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" diff --git a/Mathlib/Topology/Algebra/Order/Filter.lean b/Mathlib/Topology/Order/Filter.lean similarity index 100% rename from Mathlib/Topology/Algebra/Order/Filter.lean rename to Mathlib/Topology/Order/Filter.lean index 0c23c8e60dbe7..4a9d4af3d2134 100644 --- a/Mathlib/Topology/Algebra/Order/Filter.lean +++ b/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" diff --git a/Mathlib/Topology/Algebra/Order/IntermediateValue.lean b/Mathlib/Topology/Order/IntermediateValue.lean similarity index 100% rename from Mathlib/Topology/Algebra/Order/IntermediateValue.lean rename to Mathlib/Topology/Order/IntermediateValue.lean diff --git a/Mathlib/Topology/Algebra/Order/LeftRight.lean b/Mathlib/Topology/Order/LeftRight.lean similarity index 100% rename from Mathlib/Topology/Algebra/Order/LeftRight.lean rename to Mathlib/Topology/Order/LeftRight.lean diff --git a/Mathlib/Topology/Algebra/Order/LeftRightLim.lean b/Mathlib/Topology/Order/LeftRightLim.lean similarity index 99% rename from Mathlib/Topology/Algebra/Order/LeftRightLim.lean rename to Mathlib/Topology/Order/LeftRightLim.lean index 0e716dbf5f976..5e56c6eec1da7 100644 --- a/Mathlib/Topology/Algebra/Order/LeftRightLim.lean +++ b/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" diff --git a/Mathlib/Topology/LocalExtr.lean b/Mathlib/Topology/Order/LocalExtr.lean similarity index 99% rename from Mathlib/Topology/LocalExtr.lean rename to Mathlib/Topology/Order/LocalExtr.lean index 9835e730ac25b..19f89bb25d636 100644 --- a/Mathlib/Topology/LocalExtr.lean +++ b/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 - diff --git a/Mathlib/Topology/Algebra/Order/MonotoneContinuity.lean b/Mathlib/Topology/Order/MonotoneContinuity.lean similarity index 100% rename from Mathlib/Topology/Algebra/Order/MonotoneContinuity.lean rename to Mathlib/Topology/Order/MonotoneContinuity.lean index 80cbda7bbc02d..537a273b4b552 100644 --- a/Mathlib/Topology/Algebra/Order/MonotoneContinuity.lean +++ b/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" diff --git a/Mathlib/Topology/Algebra/Order/MonotoneConvergence.lean b/Mathlib/Topology/Order/MonotoneConvergence.lean similarity index 100% rename from Mathlib/Topology/Algebra/Order/MonotoneConvergence.lean rename to Mathlib/Topology/Order/MonotoneConvergence.lean diff --git a/Mathlib/Topology/Algebra/Order/ProjIcc.lean b/Mathlib/Topology/Order/ProjIcc.lean similarity index 100% rename from Mathlib/Topology/Algebra/Order/ProjIcc.lean rename to Mathlib/Topology/Order/ProjIcc.lean diff --git a/Mathlib/Topology/Algebra/Order/T5.lean b/Mathlib/Topology/Order/T5.lean similarity index 100% rename from Mathlib/Topology/Algebra/Order/T5.lean rename to Mathlib/Topology/Order/T5.lean index 8eea6b45784ce..46daef5e949f6 100644 --- a/Mathlib/Topology/Algebra/Order/T5.lean +++ b/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" diff --git a/Mathlib/Topology/TietzeExtension.lean b/Mathlib/Topology/TietzeExtension.lean index 26065703f84a1..187863593af9c 100644 --- a/Mathlib/Topology/TietzeExtension.lean +++ b/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"