Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-18 18:01 4f31117e

View on Github →

feat(data/set/basic): add set.subset_range_iff_exists_image_eq and set.range_image (#14203)

  • add set.subset_range_iff_exists_image_eq and set.range_image;
  • use the former to golf set.can_lift (name fixed from set.set.can_lift);
  • golf set.exists_eq_singleton_iff_nonempty_subsingleton.

Estimated changes

added theorem set.range_image