Commit 2023-11-03 20:42 f4243b97

View on Github →

feat: Lemmas about the iterated shadow (#7863) Move the lemmas characterising Covby on Finset α from Data.Finset.Interval to Data.Finset.Basic. Golf the other proofs in Data.Finset.Interval and make sure the lemma names reflect whether each lemma is about insert or cons.

Estimated changes

modified theorem Finset.mem_shadow_iff
modified theorem Finset.mem_upShadow_iff
added theorem Finset.covby_cons
added theorem Finset.covby_insert
modified theorem Finset.insert_erase
modified theorem Finset.insert_sdiff_cancel
modified theorem Finset.subset_insert
modified theorem Finset.card_eq_succ
modified theorem Finset.card_eq_three
modified theorem Finset.card_eq_two
deleted theorem Finset.antitone_iff'
deleted theorem Finset.antitone_iff
deleted theorem Finset.covby_cons
deleted theorem Finset.covby_iff'
deleted theorem Finset.covby_iff
deleted theorem Finset.covby_insert
deleted theorem Finset.monotone_iff'
deleted theorem Finset.monotone_iff
deleted theorem Finset.strictAnti_iff'
deleted theorem Finset.strictAnti_iff
deleted theorem Finset.strictMono_iff'
deleted theorem Finset.strictMono_iff