Commit 2023-09-29 06:57 b3b5ba1e

View on Github →

feat: Supremum of Finset.Iic a (#7416) and lemmas about Set.toFinset of Finset.Ixx

Estimated changes

added theorem Finset.inf'_Ici
added theorem Finset.inf_Ici
added theorem Finset.nonempty_Ici
added theorem Finset.nonempty_Iic
added theorem Finset.nonempty_Iio
added theorem Finset.nonempty_Ioi
added theorem Finset.sup'_Iic
added theorem Finset.sup_Iic
added theorem Set.toFinset_Icc
added theorem Set.toFinset_Ici
added theorem Set.toFinset_Ico
added theorem Set.toFinset_Iic
added theorem Set.toFinset_Iio
added theorem Set.toFinset_Ioc
added theorem Set.toFinset_Ioi
added theorem Set.toFinset_Ioo