Commit 2023-10-23 12:31 cf2788d1

View on Github →

feat: Pointwise set difference, complement (#7383) Define Finset.diffs and Finset.compls, the pointwise set difference of two finsets and pointwise complement of a finset. diffs appears in the statement of the Marica-Schönheim inequality and compls in the proof. Also fix the corresponding statements for sups and infs to use the new · notation.

Estimated changes

added theorem Finset.shadow_compls
deleted theorem Finset.shadow_image_compl
added theorem Finset.upShadow_compls
added theorem Finset.card_compls
added theorem Finset.card_diffs_iff
added theorem Finset.card_diffs_le
added theorem Finset.coe_compls
added theorem Finset.coe_diffs
added def Finset.compls
added theorem Finset.compls_compls
added theorem Finset.compls_empty
added theorem Finset.compls_eq_empty
added theorem Finset.compls_infs
added theorem Finset.compls_inter
added theorem Finset.compls_nonempty
added theorem Finset.compls_sups
added theorem Finset.compls_union
added theorem Finset.compls_univ
added def Finset.diffs
added theorem Finset.diffs_empty
added theorem Finset.diffs_eq_empty
added theorem Finset.diffs_nonempty
added theorem Finset.diffs_singleton
added theorem Finset.diffs_subset
added theorem Finset.empty_diffs
added theorem Finset.image_compl
modified theorem Finset.infs_singleton
added theorem Finset.mem_compls
added theorem Finset.mem_diffs
added theorem Finset.sdiff_mem_diffs
added theorem Finset.singleton_diffs
modified theorem Finset.singleton_infs
modified theorem Finset.singleton_sups
added theorem Finset.sized_compls
added theorem Finset.subset_diffs
modified theorem Finset.sups_singleton