Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-16 17:16 0eb160a5

View on Github →

feat(data/finset/basic): When insert is injective and other lemmas (#11982)

  • insert/cons lemmas for finset and multiset
  • has_ssubset instance for multiset
  • finset.sdiff_nonempty
  • disjoint.of_image_finset, finset.disjoint_image, finset.disjoint_map
  • finset.exists_eq_insert_iff
  • mem lemmas
  • change pred to - 1 into the statement of finset.card_erase_of_mem

Estimated changes

added theorem finset.cons_subset
added theorem finset.disjoint_image
added theorem finset.disjoint_map
added theorem finset.insert_inj
added theorem finset.insert_inj_on
added theorem finset.sdiff_nonempty
added theorem finset.ssubset_cons
added theorem finset.subset_cons
modified theorem finset.card_eq_succ
modified theorem finset.card_erase_eq_ite
modified theorem finset.card_erase_of_mem
added theorem multiset.ssubset_cons
added theorem multiset.subset_cons
added theorem set.insert_inj
modified theorem set.mem_of_mem_insert_of_ne
added theorem function.insert_inj_on
added theorem ne_of_mem_of_not_mem'
modified theorem ne_of_mem_of_not_mem