Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-11 21:54 ccf8aa04

View on Github →

feat(data/finset/basic): disj_Union (#16421) finset.disj_Union is to finset.bUnion as:

  • finset.disj_union is to finset.union
  • finset.cons is to insert
  • finset.map is to finset.image

Estimated changes

added theorem finset.card_disj_Union
added theorem finset.prod_disj_Union
added theorem finset.coe_disj_Union
added theorem finset.disj_Union_cons
added theorem finset.disj_Union_map
added theorem finset.disj_Union_val
added theorem finset.map_disj_Union
added theorem finset.mem_disj_Union
added theorem finset.fold_disj_Union
added theorem list.attach_map_coe'
added theorem list.attach_map_coe
added theorem list.attach_map_val'
modified theorem list.attach_map_val
modified theorem multiset.attach_map_coe
modified theorem multiset.attach_map_val
added theorem multiset.fold_bind