Mathlib v3 is deprecated. Go to Mathlib v4

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

Modified src/order/hom/basic.lean

Created src/order/hom/bounded.lean

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.cancel_left

added theorem bounded_order_hom.cancel_right

added theorem bounded_order_hom.coe_comp

added theorem bounded_order_hom.coe_comp_bot_hom

added theorem bounded_order_hom.coe_comp_order_hom

added theorem bounded_order_hom.coe_comp_top_hom

added theorem bounded_order_hom.coe_id

added def bounded_order_hom.comp

added theorem bounded_order_hom.comp_apply

added theorem bounded_order_hom.comp_assoc

added theorem bounded_order_hom.comp_id

added theorem bounded_order_hom.ext

added theorem bounded_order_hom.id_apply

added theorem bounded_order_hom.id_comp

added def bounded_order_hom.to_bot_hom

added theorem bounded_order_hom.to_fun_eq_coe

added def bounded_order_hom.to_top_hom

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

Modified src/order/hom/lattice.lean

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

deleted def bounded_lattice_hom.to_bot_hom

added def bounded_lattice_hom.to_bounded_order_hom

deleted def bounded_lattice_hom.to_top_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