introduce top level dir order: move algebra.order and content of …

…`algebra.lattice`
leanprover-community · Aug 11, 2017 · e27aae8 · e27aae8
1 parent 218c1dd
commit e27aae8
Show file tree

Hide file tree

Showing 17 changed files with 15 additions and 35 deletions.
diff --git a/algebra/lattice/README.md b/algebra/lattice/README.md
diff --git a/algebra/lattice/default.lean b/algebra/lattice/default.lean
diff --git a/data/set/lattice.lean b/data/set/lattice.lean
@@ -6,7 +6,7 @@ Authors Jeremy Avigad, Leonardo de Moura, Johannes Hölzl
 -- QUESTION: can make the first argument in ∀ x ∈ a, ... implicit?
 -/
 import logic.basic data.set.basic
-import algebra.lattice algebra.order algebra.lattice.complete_boolean_algebra category.basic
+import order.complete_boolean_algebra category.basic
 import tactic.finish
 
 open function tactic set lattice auto

diff --git a/algebra/order.lean → order/basic.lean b/algebra/order.lean → order/basic.lean
diff --git a/algebra/lattice/boolean_algebra.lean → order/boolean_algebra.lean b/algebra/lattice/boolean_algebra.lean → order/boolean_algebra.lean
@@ -5,7 +5,7 @@ Authors: Johannes Hölzl
 
 Type class hierarchy for Boolean algebras.
 -/
-import algebra.lattice.bounded_lattice
+import order.bounded_lattice
 
 set_option old_structure_cmd true
 

diff --git a/algebra/lattice/bounded_lattice.lean → order/bounded_lattice.lean b/algebra/lattice/bounded_lattice.lean → order/bounded_lattice.lean
@@ -8,7 +8,7 @@ Defines bounded lattice type class hierarchy.
 Includes the Prop and fun instances.
 -/
 
-import algebra.lattice.basic
+import order.lattice
 
 set_option old_structure_cmd true
 

diff --git a/...bra/lattice/complete_boolean_algebra.lean → order/complete_boolean_algebra.lean b/...bra/lattice/complete_boolean_algebra.lean → order/complete_boolean_algebra.lean
@@ -5,7 +5,7 @@ Authors: Johannes Hölzl
 
 Theory of complete Boolean algebras.
 -/
-import algebra.lattice.complete_lattice algebra.lattice.boolean_algebra data.set.basic
+import order.complete_lattice order.boolean_algebra data.set.basic
 
 set_option old_structure_cmd true
 

diff --git a/algebra/lattice/complete_lattice.lean → order/complete_lattice.lean b/algebra/lattice/complete_lattice.lean → order/complete_lattice.lean
@@ -5,7 +5,7 @@ Authors: Johannes Hölzl
 
 Theory of complete lattices.
 -/
-import algebra.lattice.bounded_lattice data.set.basic
+import order.bounded_lattice data.set.basic
 
 set_option old_structure_cmd true
 

diff --git a/order/default.lean b/order/default.lean
@@ -0,0 +1,3 @@
+import order.basic order.lattice order.bounded_lattice
+       order.boolean_algebra order.complete_lattice
+
diff --git a/algebra/lattice/filter.lean → order/filter.lean b/algebra/lattice/filter.lean → order/filter.lean
@@ -5,7 +5,7 @@ Authors: Johannes Hölzl
 
 Theory of filters on sets.
 -/
-import algebra.lattice.complete_lattice data.set algebra.lattice.zorn
+import order.complete_lattice data.set order.zorn
 open lattice set
 
 universes u v w x y

diff --git a/algebra/lattice/fixed_points.lean → order/fixed_points.lean b/algebra/lattice/fixed_points.lean → order/fixed_points.lean
@@ -6,7 +6,7 @@ Authors: Johannes Hölzl
 Fixed point construction on complete lattices.
 -/
 
-import algebra.lattice.complete_lattice
+import order.complete_lattice
 
 universes u v w
 variables {α : Type u} {β : Type v} {γ : Type w}

diff --git a/algebra/lattice/basic.lean → order/lattice.lean b/algebra/lattice/basic.lean → order/lattice.lean
@@ -6,7 +6,7 @@ Authors: Johannes Hölzl
 Defines the inf/sup (semi)-lattice with optionally top/bot type class hierarchy.
 -/
 
-import algebra.order tactic.finish
+import order.basic tactic.finish
 open auto
 
 set_option old_structure_cmd true

diff --git a/algebra/lattice/zorn.lean → order/zorn.lean b/algebra/lattice/zorn.lean → order/zorn.lean
diff --git a/tactic/converter/binders.lean b/tactic/converter/binders.lean
@@ -5,7 +5,7 @@ Authors: Johannes Hölzl
 
 Binder elimination
 -/
-import algebra.lattice tactic.converter.old_conv
+import order tactic.converter.old_conv
 
 namespace old_conv
 open tactic monad

diff --git a/topology/real.lean b/topology/real.lean
@@ -22,7 +22,7 @@ generalizations:
 
 -/
 
-import topology.uniform_space data.rat algebra.field algebra.order
+import topology.uniform_space data.rat algebra.field
 noncomputable theory
 open classical set lattice filter
 local attribute [instance] decidable_inhabited prop_decidable

diff --git a/topology/topological_space.lean b/topology/topological_space.lean
@@ -10,7 +10,7 @@ Parts of the formalization is based on the books:
   I. M. James: Topologies and Uniformities
 A major difference is that this formalization is heavily based on the filter library.
 -/
-import algebra.lattice.filter
+import order.filter
 open set filter lattice classical
 local attribute [instance] decidable_inhabited prop_decidable
 

diff --git a/topology/uniform_space.lean b/topology/uniform_space.lean
@@ -27,7 +27,7 @@ The formalization is mostly based on the books:
   I. M. James: Topologies and Uniformities
 A major difference is that this formalization is heavily based on the filter library.
 -/
-import algebra.lattice.filter topology.topological_space topology.continuity
+import order.filter topology.topological_space topology.continuity
 open set lattice filter classical
 local attribute [instance] decidable_inhabited prop_decidable