mathlib3

0386c3b3 - refactor(order/filter/lift): reformulate `lift_infi` etc (#14138)

refactor(order/filter/lift): reformulate `lift_infi` etc (#14138) * add `monotone.of_map_inf` and `monotone.of_map_sup`; * add `filter.lift_infi_le`: this inequality doesn't need any assumptions; * reformulate `filter.lift_infi` and `filter.lift'_infi` using `g (s ∩ t) = g s ⊓ g t` instead of `g s ⊓ g t = g (s ∩ t)`; * rename `filter.lift_infi'` to `filter.lift_infi_of_directed`, use `g (s ∩ t) = g s ⊓ g t`; * add `filter.lift_infi_of_map_univ` and `filter.lift'_infi_of_map_univ`.