mathlib3
c53285a8 - feat(order/filter/lift): drop an unneeded assumption (#14117)

Commit
3 years ago
feat(order/filter/lift): drop an unneeded assumption (#14117) Drop `monotone _` assumptions in `filter.comap_lift_eq` and `filter.comap_lift'_eq`.
Author
Parents
Loading