Commit 2022-05-22 12:23 0386c3b3

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.