Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-31 11:21 406719e9

View on Github →

feat(order/hom/lattice): Composition of lattice homs (#11676) Define top_hom.comp, bot_hom.comp, sup_hom.comp, inf_hom.comp, lattice_hom.comp, bounded_lattice_hom.comp, order_hom.to_lattice_hom.

Estimated changes

added theorem bot_hom.cancel_left
added theorem bot_hom.cancel_right
added theorem bot_hom.coe_comp
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.id_comp
added theorem inf_hom.cancel_left
added theorem inf_hom.cancel_right
added theorem inf_hom.coe_comp
added def inf_hom.comp
added theorem inf_hom.comp_apply
added theorem inf_hom.comp_assoc
added theorem inf_hom.comp_id
added theorem inf_hom.id_comp
added theorem lattice_hom.coe_comp
added def lattice_hom.comp
added theorem lattice_hom.comp_apply
added theorem lattice_hom.comp_assoc
added theorem lattice_hom.comp_id
added theorem lattice_hom.id_comp
added theorem sup_hom.cancel_left
added theorem sup_hom.cancel_right
added theorem sup_hom.coe_comp
added def sup_hom.comp
added theorem sup_hom.comp_apply
added theorem sup_hom.comp_assoc
added theorem sup_hom.comp_id
added theorem sup_hom.id_comp
added theorem top_hom.cancel_left
added theorem top_hom.cancel_right
added theorem top_hom.coe_comp
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.id_comp