feat(data/set/finite): add finite_lt_nat

leanprover-community · Mar 8, 2019 · b185829 · b185829
1 parent 7de57e8
commit b185829
Showing 1 changed file with 2 additions and 0 deletions.
diff --git 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