Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-14 10:41 7deb32cb

View on Github →

chore(data/fintype/intervals): finiteness of Ioo, Ioc, and Icc over ℕ (#9096) We already have the analogous lemmas and instance for ℤ.

Estimated changes

added theorem set.Icc_ℕ_card
added theorem set.Icc_ℕ_finite
added theorem set.Ico_ℕ_finite
added theorem set.Ioc_ℕ_card
added theorem set.Ioc_ℕ_finite
added theorem set.Ioo_ℕ_card
added theorem set.Ioo_ℕ_finite