Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-12-08 11:15 68d09c58

View on Github →

feat(data/set/pointwise/interval): generalize some lemmas (#17837)

Add set.bij_on.inter_maps_to and set.maps_to.inter_bij_on.
Generalize set.image_add_const_Ici etc to [ordered_cancel_add_comm_monoid α] [has_exists_add_of_le α].
Reorder, golf.

Estimated changes

Modified src/data/set/function.lean

modified theorem set.bij_on.bijective

added theorem set.bij_on.inter_maps_to

added theorem set.maps_to.inter_bij_on

Modified src/data/set/pointwise/interval.lean

modified theorem set.image_add_const_Ici

modified theorem set.image_add_const_Ioi