mathlib
68d09c58 - feat(data/set/pointwise/interval): generalize some lemmas (#17837)

Commit
3 years ago
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.
Author
Parents
Loading