Commit 2023-03-18 01:10 20715f4a

View on Github →

feat(data/set/sups): Set family operations (#18172) Followup to #17947. Add a similar set API (but do not define set.disj_sups because I don't need it), correct a few lemma names and connect to upper/lower sets.

Estimated changes

Modified src/data/finset/n_ary.lean

modified theorem finset.image_subset_image₂_left

modified theorem finset.image_subset_image₂_right

added theorem finset.image₂_image₂_image₂_comm

Modified src/data/finset/sups.lean

modified theorem finset.coe_infs

modified theorem finset.coe_sups

added theorem finset.disj_sups_disj_sups_disj_sups_comm

added theorem finset.empty_infs

added theorem finset.empty_sups

modified theorem finset.image_subset_infs_left

modified theorem finset.image_subset_infs_right

modified theorem finset.image_subset_sups_left

modified theorem finset.image_subset_sups_right

deleted def finset.infs

added theorem finset.infs_empty

deleted theorem finset.infs_empty_left

deleted theorem finset.infs_empty_right

added theorem finset.infs_eq_empty

deleted theorem finset.infs_eq_empty_iff

added theorem finset.infs_infs_infs_comm

added theorem finset.infs_nonempty

deleted theorem finset.infs_nonempty_iff

modified theorem finset.infs_singleton

deleted theorem finset.infs_singleton_left'

deleted theorem finset.infs_singleton_left

deleted theorem finset.infs_singleton_right

added theorem finset.infs_sups_subset_left

added theorem finset.infs_sups_subset_right

modified theorem finset.mem_infs

modified theorem finset.mem_sups

deleted theorem finset.nonempty.infs

deleted theorem finset.nonempty.sups

added theorem finset.singleton_infs

added theorem finset.singleton_infs_singleton

added theorem finset.singleton_sups

added theorem finset.singleton_sups_singleton

deleted def finset.sups

added theorem finset.sups_empty

deleted theorem finset.sups_empty_left

deleted theorem finset.sups_empty_right

added theorem finset.sups_eq_empty

deleted theorem finset.sups_eq_empty_iff

added theorem finset.sups_infs_subset_left

added theorem finset.sups_infs_subset_right

added theorem finset.sups_nonempty

deleted theorem finset.sups_nonempty_iff

modified theorem finset.sups_singleton

deleted theorem finset.sups_singleton_left'

deleted theorem finset.sups_singleton_left

deleted theorem finset.sups_singleton_right

added theorem finset.sups_sups_sups_comm

Modified src/data/set/n_ary.lean

added theorem set.image2_image2_image2_comm

Created src/data/set/sups.lean

added theorem lower_closure_infs

added theorem set.Union_image_inf_left

added theorem set.Union_image_inf_right

added theorem set.Union_image_sup_left

added theorem set.Union_image_sup_right

added theorem set.empty_infs

added theorem set.empty_sups

added theorem set.forall_infs_iff

added theorem set.forall_sups_iff

added theorem set.image_inf_prod

added theorem set.image_subset_infs_left

added theorem set.image_subset_infs_right

added theorem set.image_subset_sups_left

added theorem set.image_subset_sups_right

added theorem set.image_sup_prod

added theorem set.inf_mem_infs

added theorem set.infs_assoc

added theorem set.infs_comm

added theorem set.infs_empty

added theorem set.infs_eq_empty

added theorem set.infs_infs_infs_comm

added theorem set.infs_inter_subset_left

added theorem set.infs_inter_subset_right

added theorem set.infs_left_comm

added theorem set.infs_nonempty

added theorem set.infs_right_comm

added theorem set.infs_singleton

added theorem set.infs_subset

added theorem set.infs_subset_iff

added theorem set.infs_subset_left

added theorem set.infs_subset_right

added theorem set.infs_sups_subset_left

added theorem set.infs_sups_subset_right

added theorem set.infs_union_left

added theorem set.infs_union_right

added theorem set.mem_infs

added theorem set.mem_sups

added theorem set.nonempty.of_infs_left

added theorem set.nonempty.of_infs_right

added theorem set.nonempty.of_sups_left

added theorem set.nonempty.of_sups_right

added theorem set.singleton_infs

added theorem set.singleton_infs_singleton

added theorem set.singleton_sups

added theorem set.singleton_sups_singleton

added theorem set.sup_mem_sups

added theorem set.sups_assoc

added theorem set.sups_comm

added theorem set.sups_empty

added theorem set.sups_eq_empty

added theorem set.sups_infs_subset_left

added theorem set.sups_infs_subset_right

added theorem set.sups_inter_subset_left

added theorem set.sups_inter_subset_right

added theorem set.sups_left_comm

added theorem set.sups_nonempty

added theorem set.sups_right_comm

added theorem set.sups_singleton

added theorem set.sups_subset

added theorem set.sups_subset_iff

added theorem set.sups_subset_left

added theorem set.sups_subset_right

added theorem set.sups_sups_sups_comm

added theorem set.sups_union_left

added theorem set.sups_union_right

added theorem upper_closure_sups