Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-01-13 18:13 1990ff7e

View on Github →

feat(data/finset/sups): Set family operations (#17947) Define three binary operations on set α and finset α for use in the four functions theorem and the van den Berg-Kesten-Reimer and Ahlswede-Daykin inequalities.

Estimated changes

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.disj_sups
added theorem finset.disj_sups_assoc
added theorem finset.disj_sups_comm
added theorem finset.forall_infs_iff
added theorem finset.forall_sups_iff
added theorem finset.inf_mem_infs
added def finset.infs
added theorem finset.infs_assoc
added theorem finset.infs_comm
added theorem finset.infs_empty_left
added theorem finset.infs_left_comm
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_union_left
added theorem finset.mem_disj_sups
added theorem finset.mem_infs
added theorem finset.mem_sups
added theorem finset.nonempty.infs
added theorem finset.nonempty.sups
added theorem finset.subset_infs
added theorem finset.subset_sups
added theorem finset.sup_mem_sups
added def finset.sups
added theorem finset.sups_assoc
added theorem finset.sups_comm
added theorem finset.sups_empty_left
added theorem finset.sups_left_comm
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_union_left