Commit 2021-09-29 04:03 861d3bc4

chore(order/preorder_hom): more homs, golf a few proofs (#9256)

New preorder_homs

• preorder_hom.curry: an order isomorphism between α × β →ₘ γ and α →ₘ β →ₘ γ;
• preorder_hom.compₘ: a fully bundled version of preorder_hom.comp;
• preorder_hom.prodₘ: a fully bundled version of preorder_hom.prod;
• preorder_hom.prod_iso: Order isomorphism between the space of monotone maps to β × γ and the product of the spaces +of monotone maps to β and γ;
• preorder_hom.pi: construct a bundled monotone map α →ₘ Π i, π i from a family of monotone maps +f i : α →ₘ π i;
• preorder_hom.pi_iso: same thing, as an order_iso;
• preorder_hom.dual: interpret f : α →ₘ β as order_dual α →ₘ order_dual β;
• preorder_hom.dual_iso: same as an order_iso (with one more order_dual to get a monotone map, not an antitone map);

Renamed/moved preorder_homs

The following preorder_homs were renamed and/or moved from order.omega_complete_partial_order to order.preorder_hom.

• preorder_hom.const : moved, bundle as β →ₘ α →ₘ β;
• preorder_hom.prod.diag : preorder_hom.diag;
• preorder_hom.prod.map : preorder_hom.prod_map;
• preorder_hom.prod.fst : preorder_hom.fst;
• preorder_hom.prod.snd : preorder_hom.snd;
• preorder_hom.prod.zip : preorder_hom.prod;
• pi.monotone_apply : pi.eval_preorder_hom;
• preorder_hom.monotone_apply : preorder_hom.apply;
• preorder_hom.to_fun_hom : moved.

Other changes

• add an instance can_lift (α → β) (α →ₘ β);

• rename omega_complete_partial_order.continuous.to_monotone to omega_complete_partial_order.continuous'.to_monotone to enable dot notation, same with omega_complete_partial_order.continuous.to_bundled;

• use order_dual to get some proofs;
• golf some proofs;
• redefine has_Inf.Inf and has_Sup.Sup using infi/supr;
• generalize some mono lemmas;
• use notation →ₘ.