Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-26 20:00 75b4ee86

View on Github →

feat(data/equiv/local_equiv): construct from bij_on or inj_on (#2232)

  • feat(data/equiv/local_equiv): construct from bij_on or inj_on Also fix usage of nonempty vs inhabited in set/function. Linter didn't catch these bugs because the types use the .to_nonempty projection of the [inhabited] arguments.
  • Add simps/simp attrs

Estimated changes

modified theorem set.inj_on.inv_fun_on_image
modified theorem set.surj_on.bij_on_subset