This repository has been archived by the owner on Jul 24, 2024. It is now read-only.
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
chore(order/preorder_hom): more homs, golf a few proofs (#9256)
### New `preorder_hom`s * `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_hom`s The following `preorder_hom`s 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 `→ₘ`. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
- Loading branch information