Commit 2024-10-04 20:24 dcfb7823

View on Github →

feat: Adding/removing an element from a product of finsets (#7898) Lemmas about the interaction of Fintype.piFinset with Fin.consEquiv, Fin.snocEquiv, Fin.insertNthEquiv.

Estimated changes

Modified Mathlib/Data/Fin/Tuple/Finset.lean

modified theorem Fin.cons_mem_piFinset_cons

added theorem Fin.insertNth_mem_piFinset_insertNth

added theorem Fin.mem_piFinset_iff_last_init

added theorem Fin.mem_piFinset_iff_pivot_removeNth

added theorem Fin.mem_piFinset_iff_zero_tail

deleted theorem Fin.mem_piFinset_succ'

deleted theorem Fin.mem_piFinset_succ

modified theorem Fin.snoc_mem_piFinset_snoc

added theorem Finset.card_consEquiv_filter_piFinset

added theorem Finset.card_insertNthEquiv_filter_piFinset

added theorem Finset.card_snocEquiv_filter_piFinset

added theorem Finset.map_consEquiv_filter_piFinset

added theorem Finset.map_insertNthEquiv_filter_piFinset

added theorem Finset.map_snocEquiv_filter_piFinset