diff --git a/src/data/set/finite.lean b/src/data/set/finite.lean
index fb22722e41ce6..30b1a0de30fac 100644
--- a/src/data/set/finite.lean
+++ b/src/data/set/finite.lean
@@ -268,6 +268,8 @@ by simpa [nat.lt_succ_iff] using set.fintype_lt_nat (n+1)
 
 lemma finite_le_nat (n : ℕ) : finite {i | i ≤ n} := ⟨set.fintype_le_nat _⟩
 
+lemma finite_lt_nat (n : ℕ) : finite {i | i < n} := ⟨set.fintype_lt_nat _⟩
+
 instance fintype_prod (s : set α) (t : set β) [fintype s] [fintype t] : fintype (set.prod s t) :=
 fintype_of_finset (s.to_finset.product t.to_finset) $ by simp