chore(data/{finset,multiset}/locally_finite): rename from .interval (…

…#9980) The pattern is `data.stuff.interval` for files about `locally_finite_order stuff` and... `finset α` and `multiset α` are locally finite orders. This thus makes space for this theory.
leanprover-community · Oct 26, 2021 · ce164e2 · ce164e2
1 parent 3aa5749
commit ce164e2
Show file tree

Hide file tree

Showing 4 changed files with 4 additions and 4 deletions.
diff --git a/src/data/finset/default.lean b/src/data/finset/default.lean
@@ -1,7 +1,7 @@
 import data.finset.basic
 import data.finset.fold
-import data.finset.interval
 import data.finset.lattice
+import data.finset.locally_finite
 import data.finset.nat_antidiagonal
 import data.finset.pi
 import data.finset.powerset

diff --git a/src/data/finset/interval.lean → src/data/finset/locally_finite.lean b/src/data/finset/interval.lean → src/data/finset/locally_finite.lean
diff --git a/src/data/multiset/interval.lean → src/data/multiset/locally_finite.lean b/src/data/multiset/interval.lean → src/data/multiset/locally_finite.lean
@@ -3,7 +3,7 @@ Copyright (c) 2021 Yaël Dillies. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
-import data.finset.interval
+import data.finset.locally_finite
 
 /-!
 # Intervals as multisets

diff --git a/src/data/nat/interval.lean b/src/data/nat/interval.lean
@@ -3,7 +3,7 @@ Copyright (c) 2021 Yaël Dillies. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
-import data.finset.interval
+import data.finset.locally_finite
 
 /-!
 # Finite intervals of naturals
@@ -14,7 +14,7 @@ intervals as finsets and fintypes.
 ## TODO
 
 Some lemmas can be generalized using `ordered_group`, `canonically_ordered_monoid` or `succ_order`
-and subsequently be moved upstream to `data.finset.interval`.
+and subsequently be moved upstream to `data.finset.locally_finite`.
 -/
 
 open finset nat