Commit 2023-09-28 05:09 51e00c7c

View on Github →

feat: Extra sups lemmas (#7382)

Estimated changes

added theorem Finset.filter_infs_le
added theorem Finset.filter_sups_le
added theorem Finset.image_infs
added theorem Finset.image_sups
added theorem Finset.infs_self
added theorem Finset.map_infs
added theorem Finset.map_sups
added theorem Finset.powerset_inter
added theorem Finset.powerset_union
added theorem Finset.sups_eq_self
added theorem Set.image_infs
added theorem Set.image_sups
added theorem Set.infs_self
added theorem Set.infs_self_subset
added theorem Set.sep_infs_le
added theorem Set.sep_sups_le
added theorem Set.subset_infs_self
added theorem Set.subset_sups_self
added theorem Set.sups_eq_self
added theorem Set.sups_subset_self
added theorem IsLowerSet.infClosed
added theorem IsUpperSet.supClosed