lift): add `lift_map_le`, `lift'_map_le` (#17488)

Commit

3 years ago

feat(order/filter/lift): add `lift_map_le`, `lift'_map_le` (#17488) Also golf `map_lift_eq2`.

Author

urkud

Parents