move(analysis/normed/order/basic): Move from `analysis.normed_space.o…

…rdered` (#17239) Rename `analysis.normed_space.ordered` to `analysis.normed.order.basic` because: * It wasn't mentioning `normed_space` at all * I am about to add properties of upper/lower sets in normed ordered groups
leanprover-community · Oct 29, 2022 · 76ec0e5 · 76ec0e5
1 parent 62c0a4e
commit 76ec0e5
Show file tree

Hide file tree

Showing 7 changed files with 6 additions and 6 deletions.
diff --git a/src/analysis/asymptotics/asymptotic_equivalent.lean b/src/analysis/asymptotics/asymptotic_equivalent.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Anatole Dedecker
 -/
 import analysis.asymptotics.asymptotics
-import analysis.normed_space.ordered
+import analysis.normed.order.basic
 
 /-!
 # Asymptotic equivalence

diff --git a/src/analysis/asymptotics/specific_asymptotics.lean b/src/analysis/asymptotics/specific_asymptotics.lean
@@ -3,7 +3,7 @@ Copyright (c) 2021 Anatole Dedecker. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Anatole Dedecker
 -/
-import analysis.normed_space.ordered
+import analysis.normed.order.basic
 import analysis.asymptotics.asymptotics
 
 /-!

diff --git a/src/analysis/asymptotics/superpolynomial_decay.lean b/src/analysis/asymptotics/superpolynomial_decay.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Devon Tuma
 -/
 import analysis.asymptotics.asymptotics
-import analysis.normed_space.ordered
+import analysis.normed.order.basic
 import data.polynomial.eval
 import topology.algebra.order.liminf_limsup
 

diff --git a/src/analysis/convex/exposed.lean b/src/analysis/convex/exposed.lean
@@ -5,7 +5,7 @@ Authors: Yaël Dillies, Bhavik Mehta
 -/
 import analysis.convex.extreme
 import analysis.convex.function
-import analysis.normed_space.ordered
+import analysis.normed.order.basic
 
 /-!
 # Exposed sets

diff --git a/src/analysis/convex/strict_convex_space.lean b/src/analysis/convex/strict_convex_space.lean
@@ -5,7 +5,7 @@ Authors: Yaël Dillies, Yury Kudryashov
 -/
 import analysis.convex.strict
 import analysis.convex.topology
-import analysis.normed_space.ordered
+import analysis.normed.order.basic
 import analysis.normed_space.pointwise
 import analysis.normed_space.affine_isometry
 

diff --git a/src/analysis/locally_convex/basic.lean b/src/analysis/locally_convex/basic.lean
@@ -6,7 +6,7 @@ Authors: Jean Lo, Bhavik Mehta, Yaël Dillies
 import analysis.convex.basic
 import analysis.convex.hull
 import analysis.normed_space.lattice_ordered_group
-import analysis.normed_space.ordered
+import analysis.normed.order.basic
 
 /-!
 # Local convexity

diff --git a/src/analysis/normed_space/ordered.lean → src/analysis/normed/order/basic.lean b/src/analysis/normed_space/ordered.lean → src/analysis/normed/order/basic.lean