Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-13 13:35 324a605f

View on Github →

chore(order): rename preorder_hom to order_hom (#10750) For consistency with order_embedding and order_iso, this PR renames preorder_hom to order_hom, at the request of @YaelDillies.

Estimated changes

added def order_hom.gfp
added theorem order_hom.gfp_gfp
added theorem order_hom.gfp_le
added theorem order_hom.gfp_le_map
added theorem order_hom.is_least_lfp
added theorem order_hom.le_gfp
added theorem order_hom.le_lfp
added def order_hom.lfp
added theorem order_hom.lfp_le
added theorem order_hom.lfp_le_fixed
added theorem order_hom.lfp_le_map
added theorem order_hom.lfp_lfp
added theorem order_hom.map_gfp
added theorem order_hom.map_gfp_comp
added theorem order_hom.map_le_gfp
added theorem order_hom.map_le_lfp
added theorem order_hom.map_lfp
added theorem order_hom.map_lfp_comp
deleted def preorder_hom.gfp
deleted theorem preorder_hom.gfp_gfp
deleted theorem preorder_hom.gfp_le
deleted theorem preorder_hom.gfp_le_map
deleted theorem preorder_hom.is_least_lfp
deleted theorem preorder_hom.le_gfp
deleted theorem preorder_hom.le_lfp
deleted def preorder_hom.lfp
deleted theorem preorder_hom.lfp_le
deleted theorem preorder_hom.lfp_le_fixed
deleted theorem preorder_hom.lfp_le_map
deleted theorem preorder_hom.lfp_lfp
deleted theorem preorder_hom.map_gfp
deleted theorem preorder_hom.map_gfp_comp
deleted theorem preorder_hom.map_le_gfp
deleted theorem preorder_hom.map_le_lfp
deleted theorem preorder_hom.map_lfp
deleted theorem preorder_hom.map_lfp_comp
added def order_hom.bind
deleted def preorder_hom.bind
added theorem order_hom.Inf_apply
added theorem order_hom.Sup_apply
added def order_hom.apply
added theorem order_hom.apply_mono
added theorem order_hom.coe_fun_mk
added theorem order_hom.coe_infi
added theorem order_hom.coe_le_coe
added theorem order_hom.coe_supr
added def order_hom.comp
added theorem order_hom.comp_const
added theorem order_hom.comp_id
added theorem order_hom.comp_mono
added def order_hom.const
added theorem order_hom.const_comp
added def order_hom.curry
added theorem order_hom.curry_apply
added def order_hom.diag
added theorem order_hom.ext
added def order_hom.fst
added theorem order_hom.fst_prod_snd
added def order_hom.id
added theorem order_hom.id_comp
added theorem order_hom.infi_apply
added theorem order_hom.le_def
added theorem order_hom.mk_le_mk
added def order_hom.pi
added def order_hom.pi_iso
added theorem order_hom.prod_mono
added def order_hom.snd
added theorem order_hom.supr_apply
added def order_hom.unique
added structure order_hom
deleted theorem preorder_hom.Inf_apply
deleted theorem preorder_hom.Sup_apply
deleted def preorder_hom.apply
deleted theorem preorder_hom.apply_mono
deleted theorem preorder_hom.coe_fun_mk
deleted theorem preorder_hom.coe_infi
deleted theorem preorder_hom.coe_le_coe
deleted theorem preorder_hom.coe_supr
deleted def preorder_hom.comp
deleted theorem preorder_hom.comp_const
deleted theorem preorder_hom.comp_id
deleted theorem preorder_hom.comp_mono
deleted def preorder_hom.const
deleted theorem preorder_hom.const_comp
deleted def preorder_hom.curry
deleted theorem preorder_hom.curry_apply
deleted def preorder_hom.diag
deleted theorem preorder_hom.ext
deleted def preorder_hom.fst
deleted theorem preorder_hom.fst_prod_snd
deleted def preorder_hom.id
deleted theorem preorder_hom.id_comp
deleted theorem preorder_hom.infi_apply
deleted theorem preorder_hom.le_def
deleted theorem preorder_hom.mk_le_mk
deleted def preorder_hom.pi
deleted def preorder_hom.pi_iso
deleted theorem preorder_hom.prod_mono
deleted def preorder_hom.snd
deleted theorem preorder_hom.supr_apply
deleted def preorder_hom.unique
deleted structure preorder_hom