Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-26 11:25 20aae835

View on Github →

feat(order/hom/lattice): Lattice homomorphisms (#11610) This defines (bounded) lattice homomorphisms using the fun_like along with weaker homomorphisms that only preserve sup, inf, top, bot.

Estimated changes

added theorem bot_hom.bot_apply
added theorem bot_hom.coe_bot
added theorem bot_hom.coe_id
added theorem bot_hom.coe_inf
added theorem bot_hom.coe_sup
added theorem bot_hom.ext
added theorem bot_hom.id_apply
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 structure bounded_lattice_hom
added theorem inf_hom.coe_const
added theorem inf_hom.coe_id
added theorem inf_hom.coe_inf
added def inf_hom.const
added theorem inf_hom.const_apply
added theorem inf_hom.ext
added theorem inf_hom.id_apply
added theorem inf_hom.inf_apply
added theorem inf_hom.to_fun_eq_coe
added structure inf_hom
added theorem lattice_hom.coe_id
added theorem lattice_hom.ext
added theorem lattice_hom.id_apply
added structure lattice_hom
added theorem sup_hom.coe_const
added theorem sup_hom.coe_id
added theorem sup_hom.coe_sup
added def sup_hom.const
added theorem sup_hom.const_apply
added theorem sup_hom.ext
added theorem sup_hom.id_apply
added theorem sup_hom.sup_apply
added theorem sup_hom.to_fun_eq_coe
added structure sup_hom
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 theorem top_hom.ext
added theorem top_hom.id_apply
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