Commit 2023-03-23 14:35 1d503629

View on Github →

feat: port Data.Set.Sups (#2991)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Set/Sups.lean

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.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.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 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 lowerClosure_infs

added theorem upperClosure_sups