Commit 2023-01-17 09:34 afa19001

View on Github →

feat: port Order.Hom.Bounded (#888) mathlib3 SHA : f1a2caaf51ef593799107fe9a8d5e411599f3996

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Hom/Bounded.lean

added theorem BotHom.bot_apply

added theorem BotHom.cancel_left

added theorem BotHom.cancel_right

added theorem BotHom.coe_bot

added theorem BotHom.coe_comp

added theorem BotHom.coe_copy

added theorem BotHom.coe_id

added theorem BotHom.coe_inf

added theorem BotHom.coe_sup

added def BotHom.comp

added theorem BotHom.comp_apply

added theorem BotHom.comp_assoc

added theorem BotHom.comp_id

added theorem BotHom.copy_eq

added theorem BotHom.dual_comp

added theorem BotHom.dual_id

added theorem BotHom.ext

added theorem BotHom.id_apply

added theorem BotHom.id_comp

added theorem BotHom.inf_apply

added theorem BotHom.sup_apply

added theorem BotHom.symm_dual_comp

added theorem BotHom.symm_dual_id

added structure BotHom

added def BotHomClass.toBotHom

added theorem BoundedOrderHom.cancel_left

added theorem BoundedOrderHom.cancel_right

added theorem BoundedOrderHom.coe_comp

added theorem BoundedOrderHom.coe_comp_bot_hom

added theorem BoundedOrderHom.coe_comp_order_hom

added theorem BoundedOrderHom.coe_comp_top_hom

added theorem BoundedOrderHom.coe_copy

added theorem BoundedOrderHom.coe_id

added def BoundedOrderHom.comp

added theorem BoundedOrderHom.comp_apply

added theorem BoundedOrderHom.comp_assoc

added theorem BoundedOrderHom.comp_id

added theorem BoundedOrderHom.copy_eq

added theorem BoundedOrderHom.dual_comp

added theorem BoundedOrderHom.dual_id

added theorem BoundedOrderHom.ext

added theorem BoundedOrderHom.id_apply

added theorem BoundedOrderHom.id_comp

added theorem BoundedOrderHom.symm_dual_comp

added theorem BoundedOrderHom.symm_dual_id

added def BoundedOrderHom.toBotHom

added def BoundedOrderHom.toTopHom

added structure BoundedOrderHom

added def BoundedOrderHomClass.toBoundedOrderHom

added theorem TopHom.cancel_left

added theorem TopHom.cancel_right

added theorem TopHom.coe_comp

added theorem TopHom.coe_copy

added theorem TopHom.coe_id

added theorem TopHom.coe_inf

added theorem TopHom.coe_sup

added theorem TopHom.coe_top

added def TopHom.comp

added theorem TopHom.comp_apply

added theorem TopHom.comp_assoc

added theorem TopHom.comp_id

added theorem TopHom.copy_eq

added theorem TopHom.dual_comp

added theorem TopHom.dual_id

added theorem TopHom.ext

added theorem TopHom.id_apply

added theorem TopHom.id_comp

added theorem TopHom.inf_apply

added theorem TopHom.sup_apply

added theorem TopHom.symm_dual_comp

added theorem TopHom.symm_dual_id

added theorem TopHom.top_apply

added structure TopHom

added def TopHomClass.toTopHom

added theorem map_eq_bot_iff

added theorem map_eq_top_iff