Commit 2023-04-08 12:22 536275b6

View on Github →

feat: port Data.Finset.Sups (#1663)

depends on: https://github.com/leanprover-community/mathlib/pull/18172
depends on: #2991

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Finset/Sups.lean

added theorem Finset.Nonempty.of_disjSups_left

added theorem Finset.Nonempty.of_disjSups_right

added theorem Finset.Nonempty.of_infs_left

added theorem Finset.Nonempty.of_infs_right

added theorem Finset.Nonempty.of_sups_left

added theorem Finset.Nonempty.of_sups_right

added theorem Finset.bunionᵢ_image_inf_left

added theorem Finset.bunionᵢ_image_inf_right

added theorem Finset.bunionᵢ_image_sup_left

added theorem Finset.bunionᵢ_image_sup_right

added theorem Finset.card_disjSups_le

added theorem Finset.card_infs_iff

added theorem Finset.card_infs_le

added theorem Finset.card_sups_iff

added theorem Finset.card_sups_le

added theorem Finset.coe_infs

added theorem Finset.coe_sups

added def Finset.disjSups

added theorem Finset.disjSups_assoc

added theorem Finset.disjSups_comm

added theorem Finset.disjSups_disjSups_disjSups_comm

added theorem Finset.disjSups_empty_left

added theorem Finset.disjSups_empty_right

added theorem Finset.disjSups_inter_subset_left

added theorem Finset.disjSups_inter_subset_right

added theorem Finset.disjSups_left_comm

added theorem Finset.disjSups_right_comm

added theorem Finset.disjSups_singleton

added theorem Finset.disjSups_subset

added theorem Finset.disjSups_subset_iff

added theorem Finset.disjSups_subset_left

added theorem Finset.disjSups_subset_right

added theorem Finset.disjSups_subset_sups

added theorem Finset.disjSups_union_left

added theorem Finset.disjSups_union_right

added theorem Finset.empty_infs

added theorem Finset.empty_sups

added theorem Finset.forall_disjSups_iff

added theorem Finset.forall_infs_iff

added theorem Finset.forall_sups_iff

added theorem Finset.image_inf_product

added theorem Finset.image_subset_infs_left

added theorem Finset.image_subset_infs_right

added theorem Finset.image_subset_sups_left

added theorem Finset.image_subset_sups_right

added theorem Finset.image_sup_product

added theorem Finset.inf_mem_infs

added theorem Finset.infs_assoc

added theorem Finset.infs_comm

added theorem Finset.infs_empty

added theorem Finset.infs_eq_empty

added theorem Finset.infs_infs_infs_comm

added theorem Finset.infs_inter_subset_left

added theorem Finset.infs_inter_subset_right

added theorem Finset.infs_left_comm

added theorem Finset.infs_nonempty

added theorem Finset.infs_right_comm

added theorem Finset.infs_singleton

added theorem Finset.infs_subset

added theorem Finset.infs_subset_iff

added theorem Finset.infs_subset_left

added theorem Finset.infs_subset_right

added theorem Finset.infs_sups_subset_left

added theorem Finset.infs_sups_subset_right

added theorem Finset.infs_union_left

added theorem Finset.infs_union_right

added theorem Finset.mem_disjSups

added theorem Finset.mem_infs

added theorem Finset.mem_sups

added theorem Finset.singleton_infs

added theorem Finset.singleton_infs_singleton

added theorem Finset.singleton_sups

added theorem Finset.singleton_sups_singleton

added theorem Finset.subset_infs

added theorem Finset.subset_sups

added theorem Finset.sup_mem_sups

added theorem Finset.sups_assoc

added theorem Finset.sups_comm

added theorem Finset.sups_empty

added theorem Finset.sups_eq_empty

added theorem Finset.sups_infs_subset_left

added theorem Finset.sups_infs_subset_right

added theorem Finset.sups_inter_subset_left

added theorem Finset.sups_inter_subset_right

added theorem Finset.sups_left_comm

added theorem Finset.sups_nonempty

added theorem Finset.sups_right_comm

added theorem Finset.sups_singleton

added theorem Finset.sups_subset

added theorem Finset.sups_subset_iff

added theorem Finset.sups_subset_left

added theorem Finset.sups_subset_right

added theorem Finset.sups_sups_sups_comm

added theorem Finset.sups_union_left

added theorem Finset.sups_union_right