Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-22 10:50 80591d65

View on Github →

feat(order/hom/lattice): Finitary join-/meet-preserving maps (#12149) Define sup_bot_hom, inf_top_hom and their associated class.

Estimated changes

added def order_bot.lift
added def order_top.lift
deleted def bounded_order.lift
deleted def order_bot.lift
deleted def order_top.lift
added theorem inf_hom.bot_apply
added theorem inf_hom.coe_bot
added theorem inf_hom.coe_top
added theorem inf_hom.top_apply
added theorem inf_top_hom.coe_comp
added theorem inf_top_hom.coe_id
added theorem inf_top_hom.coe_inf
added theorem inf_top_hom.coe_top
added def inf_top_hom.comp
added theorem inf_top_hom.comp_apply
added theorem inf_top_hom.comp_assoc
added theorem inf_top_hom.comp_id
added theorem inf_top_hom.ext
added theorem inf_top_hom.id_apply
added theorem inf_top_hom.id_comp
added theorem inf_top_hom.inf_apply
added theorem inf_top_hom.top_apply
added structure inf_top_hom
added theorem map_finset_inf
added theorem map_finset_sup
added theorem sup_bot_hom.bot_apply
added theorem sup_bot_hom.coe_bot
added theorem sup_bot_hom.coe_comp
added theorem sup_bot_hom.coe_id
added theorem sup_bot_hom.coe_sup
added def sup_bot_hom.comp
added theorem sup_bot_hom.comp_apply
added theorem sup_bot_hom.comp_assoc
added theorem sup_bot_hom.comp_id
added theorem sup_bot_hom.ext
added theorem sup_bot_hom.id_apply
added theorem sup_bot_hom.id_comp
added theorem sup_bot_hom.sup_apply
added structure sup_bot_hom
added theorem sup_hom.bot_apply
added theorem sup_hom.coe_bot
added theorem sup_hom.coe_top
modified theorem sup_hom.sup_apply
added theorem sup_hom.top_apply