Commit 2022-06-12 11:53 8cad81ae

View on Github →

feat(data/{finset,set}/basic): More insert and erase lemmas (#14675) Also turn finset.disjoint_iff_disjoint_coe around and change set.finite.to_finset_insert take (insert a s).finite instead of s.finite.

Estimated changes

Modified src/algebra/big_operators/finprod.lean

Modified src/data/finset/basic.lean

added theorem finset.disjoint_coe

deleted theorem finset.disjoint_iff_disjoint_coe

added theorem finset.erase_cons

added theorem finset.erase_image_subset_image_erase

added theorem finset.erase_inj_on'

added theorem finset.erase_ssubset_insert

added theorem finset.erase_subset_iff_of_mem

added theorem finset.filter_inter_distrib

modified theorem finset.image_inter

added theorem finset.image_inter_of_inj_on

added theorem finset.pair_eq_singleton

deleted theorem finset.pair_self_eq

added theorem finset.pairwise_disjoint_coe

added theorem finset.subset_insert_iff_of_not_mem

Modified src/data/finset/pointwise.lean

Modified src/data/fintype/basic.lean

added theorem finset.coe_eq_univ

modified theorem finset.eq_univ_iff_forall

added theorem finset.eq_univ_of_forall

added theorem finset.image_univ_of_surjective

Modified src/data/set/basic.lean

added theorem set.insert_idem

Modified src/data/set/finite.lean

added theorem set.finite.to_finset_insert'

modified theorem set.finite.to_finset_insert

added theorem set.finite.to_finset_singleton

Modified src/data/set/lattice.lean

modified theorem set.Inter_comm

added theorem set.Inter₂_comm

modified theorem set.Union_comm

added theorem set.Union₂_comm

Modified src/group_theory/perm/cycle/basic.lean

Modified src/group_theory/perm/support.lean

Modified src/logic/basic.lean

added theorem exists₂_comm

Modified src/order/complete_lattice.lean

added theorem infi₂_comm

added theorem supr₂_comm