Commit 2023-01-17 11:42 c211d671

View on Github →

feat: port Combinatorics.SetFamily.Compression.Down (#1604) Some proofs here needed rewriting mostly due to Finset.filter now taking bools and Function.comp not being seen through (see Zulip for what I think is a related discussion.)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Combinatorics/SetFamily/Compression/Down.lean

added theorem Down.card_compression

added def Down.compression

added theorem Down.compression_idem

added theorem Down.erase_mem_compression

added theorem Down.erase_mem_compression_of_mem_compression

added theorem Down.mem_compression

added theorem Down.mem_compression_of_insert_mem_compression

added theorem Finset.card_memberSubfamily_add_card_nonMemberSubfamily

added theorem Finset.mem_memberSubfamily

added theorem Finset.mem_nonMemberSubfamily

added def Finset.memberSubfamily

added theorem Finset.memberSubfamily_inter

added theorem Finset.memberSubfamily_memberSubfamily

added theorem Finset.memberSubfamily_nonMemberSubfamily

added theorem Finset.memberSubfamily_union

added theorem Finset.memberSubfamily_union_nonMemberSubfamily

added def Finset.nonMemberSubfamily

added theorem Finset.nonMemberSubfamily_inter

added theorem Finset.nonMemberSubfamily_memberSubfamily

added theorem Finset.nonMemberSubfamily_nonMemberSubfamily

added theorem Finset.nonMemberSubfamily_union