Commit 2022-02-09 23:10 4e8d8faa

View on Github →

feat(order/hom/bounded): Bounded order homomorphisms (#11806) Define bounded_order_hom in order.hom.bounded and move top_hom, bot_hom there.

Estimated changes

added theorem bot_hom.bot_apply
added theorem bot_hom.cancel_left
added theorem bot_hom.cancel_right
added theorem bot_hom.coe_bot
added theorem bot_hom.coe_comp
added theorem bot_hom.coe_id
added theorem bot_hom.coe_inf
added theorem bot_hom.coe_sup
added def bot_hom.comp
added theorem bot_hom.comp_apply
added theorem bot_hom.comp_assoc
added theorem bot_hom.comp_id
added theorem bot_hom.ext
added theorem bot_hom.id_apply
added theorem bot_hom.id_comp
added theorem bot_hom.inf_apply
added theorem bot_hom.sup_apply
added theorem bot_hom.to_fun_eq_coe
added structure bot_hom
added theorem bounded_order_hom.ext
added structure bounded_order_hom
added theorem top_hom.cancel_left
added theorem top_hom.cancel_right
added theorem top_hom.coe_comp
added theorem top_hom.coe_id
added theorem top_hom.coe_inf
added theorem top_hom.coe_sup
added theorem top_hom.coe_top
added def top_hom.comp
added theorem top_hom.comp_apply
added theorem top_hom.comp_assoc
added theorem top_hom.comp_id
added theorem top_hom.ext
added theorem top_hom.id_apply
added theorem top_hom.id_comp
added theorem top_hom.inf_apply
added theorem top_hom.sup_apply
added theorem top_hom.to_fun_eq_coe
added theorem top_hom.top_apply
added structure top_hom
deleted theorem bot_hom.bot_apply
deleted theorem bot_hom.cancel_left
deleted theorem bot_hom.cancel_right
deleted theorem bot_hom.coe_bot
deleted theorem bot_hom.coe_comp
deleted theorem bot_hom.coe_id
deleted theorem bot_hom.coe_inf
deleted theorem bot_hom.coe_sup
deleted def bot_hom.comp
deleted theorem bot_hom.comp_apply
deleted theorem bot_hom.comp_assoc
deleted theorem bot_hom.comp_id
deleted theorem bot_hom.ext
deleted theorem bot_hom.id_apply
deleted theorem bot_hom.id_comp
deleted theorem bot_hom.inf_apply
deleted theorem bot_hom.sup_apply
deleted theorem bot_hom.to_fun_eq_coe
deleted structure bot_hom
modified theorem inf_hom.cancel_left
modified theorem inf_hom.cancel_right
modified theorem lattice_hom.cancel_left
modified theorem lattice_hom.cancel_right
modified theorem sup_hom.cancel_left
modified theorem sup_hom.cancel_right
deleted theorem top_hom.cancel_left
deleted theorem top_hom.cancel_right
deleted theorem top_hom.coe_comp
deleted theorem top_hom.coe_id
deleted theorem top_hom.coe_inf
deleted theorem top_hom.coe_sup
deleted theorem top_hom.coe_top
deleted def top_hom.comp
deleted theorem top_hom.comp_apply
deleted theorem top_hom.comp_assoc
deleted theorem top_hom.comp_id
deleted theorem top_hom.ext
deleted theorem top_hom.id_apply
deleted theorem top_hom.id_comp
deleted theorem top_hom.inf_apply
deleted theorem top_hom.sup_apply
deleted theorem top_hom.to_fun_eq_coe
deleted theorem top_hom.top_apply
deleted structure top_hom