Commit 2023-10-12 21:38 c98e6b7f

View on Github →

feat: Finset family induction (#7522) Provide an induction principle for finset families: One can increase the support of a finset family one by one.

Estimated changes

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

added theorem Finset.image_insert_memberSubfamily

added theorem Finset.memberFamily_induction_on

added theorem Finset.memberSubfamily_image_erase

added theorem Finset.memberSubfamily_image_insert

added theorem Finset.nonMemberSubfamily_image_insert

Modified Mathlib/Data/Finset/Basic.lean

added theorem Finset.insert_subset_insert_iff

Modified Mathlib/Data/Set/Basic.lean

modified theorem Set.insert_subset_insert_iff