diff --git a/src/data/finset/default.lean b/src/data/finset/default.lean
index 9450420fae5cf..fb51ca936bb36 100644
--- 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 b/src/data/finset/locally_finite.lean
similarity index 100%
rename from src/data/finset/interval.lean
rename to src/data/finset/locally_finite.lean
diff --git a/src/data/multiset/interval.lean b/src/data/multiset/locally_finite.lean
similarity index 98%
rename from src/data/multiset/interval.lean
rename to src/data/multiset/locally_finite.lean
index 0171872d6b22b..cd33d23baabbb 100644
--- a/src/data/multiset/interval.lean
+++ b/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
index f710f95ba9b06..1f779981de02e 100644
--- 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