Commit 2022-01-07 18:21 5cbfddd3

View on Github →

feat(data/finset/sym): Symmetric powers of a finset (#11142) This defines finset.sym and finset.sym2, which are the finset analogs of sym and sym2, in a new file data.finset.sym.

Estimated changes

Modified src/data/finset/basic.lean

added theorem finset.disjoint_filter_filter_neg

Modified src/data/finset/prod.lean

added theorem finset.diag_union_off_diag

added theorem finset.disjoint_diag_off_diag

added theorem finset.product_eq_empty

Created src/data/finset/sym.lean

added theorem finset.diag_mem_sym2_iff

added theorem finset.eq_empty_of_sym_eq_empty

added theorem finset.image_diag_union_image_off_diag

added theorem finset.is_diag_mk_of_mem_diag

added theorem finset.mem_sym2_iff

added theorem finset.mem_sym_iff

added theorem finset.mk_mem_sym2_iff

added theorem finset.not_is_diag_mk_of_mem_off_diag

added theorem finset.repeat_mem_sym

added theorem finset.sym2_empty

added theorem finset.sym2_eq_empty

added theorem finset.sym2_mono

added theorem finset.sym2_nonempty

added theorem finset.sym2_singleton

added theorem finset.sym2_univ

added theorem finset.sym_empty

added theorem finset.sym_eq_empty

added theorem finset.sym_inter

added theorem finset.sym_mono

added theorem finset.sym_nonempty

added theorem finset.sym_singleton

added theorem finset.sym_succ

added theorem finset.sym_union

added theorem finset.sym_univ

added theorem finset.sym_zero

Modified src/data/sym/basic.lean

added theorem sym.coe_repeat

added theorem sym.eq_repeat_iff

added theorem sym.mem_repeat

Modified src/data/sym/card.lean

added theorem finset.card_sym2

modified theorem sym2.card_image_diag

Modified src/data/sym/sym2.lean

added theorem sym2.ball

added theorem sym2.out_fst_mem

added theorem sym2.out_snd_mem