Commit 2024-06-07 06:15 f415ad76

View on Github →

feat(Set,Finset): add lemmas, golf (#13591)

New lemmas

  • Set.image_nontrivial
  • Finset.map_ssubset_map, Finset.map_nontrivial

New gcongr attrs

  • Finset.map_subset_map, Finset.map_ssubset_map (.mpr implications);
  • Finset.product_subset_product_left, Finset.product_subset_product_right

Misc

  • Finset.Nonempty.map is now protected

Estimated changes

modified theorem Finset.image_eq_empty
modified theorem Finset.image_nonempty
modified theorem Finset.map_eq_empty
modified theorem Finset.map_nonempty
added theorem Finset.map_nontrivial
added theorem Finset.map_ssubset_map
added theorem Set.image_nontrivial