Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-26 10:16 61897aef

View on Github →

feat(data/set/intervals/infinite): intervals are infinite (#4241)

Estimated changes

Modified src/data/fintype/basic.lean

added theorem finset.exists_maximal

added theorem finset.exists_minimal

Modified src/data/set/finite.lean

added theorem set.finite.to_finset.nonempty

added theorem set.infinite_mono

Created src/data/set/intervals/infinite.lean

added theorem set.Icc.infinite

added theorem set.Ici.infinite

added theorem set.Ico.infinite

added theorem set.Iic.infinite

added theorem set.Iio.infinite

added theorem set.Ioc.infinite

added theorem set.Ioi.infinite

added theorem set.Ioo.infinite