Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-31 14:14 ada43f00

View on Github →

feat(order/hom/complete_lattice): Complete lattice homomorphisms (#11741) Define frame homs and complete lattice homs using the fun_like along with weaker homomorphisms that only preserve Sup, Inf.

Estimated changes

added theorem Inf_hom.cancel_left
added theorem Inf_hom.cancel_right
added theorem Inf_hom.coe_comp
added theorem Inf_hom.coe_id
added theorem Inf_hom.coe_top
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.ext
added theorem Inf_hom.id_apply
added theorem Inf_hom.id_comp
added theorem Inf_hom.to_fun_eq_coe
added theorem Inf_hom.top_apply
added structure Inf_hom
added theorem Sup_hom.bot_apply
added theorem Sup_hom.cancel_left
added theorem Sup_hom.cancel_right
added theorem Sup_hom.coe_bot
added theorem Sup_hom.coe_comp
added theorem Sup_hom.coe_id
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.ext
added theorem Sup_hom.id_apply
added theorem Sup_hom.id_comp
added theorem Sup_hom.to_fun_eq_coe
added structure Sup_hom
added structure complete_lattice_hom
added theorem frame_hom.bot_apply
added theorem frame_hom.cancel_left
added theorem frame_hom.cancel_right
added theorem frame_hom.coe_bot
added theorem frame_hom.coe_comp
added theorem frame_hom.coe_id
added def frame_hom.comp
added theorem frame_hom.comp_apply
added theorem frame_hom.comp_assoc
added theorem frame_hom.comp_id
added theorem frame_hom.ext
added theorem frame_hom.id_apply
added theorem frame_hom.id_comp
added structure frame_hom
added theorem map_infi
added theorem map_infi₂
added theorem map_supr
added theorem map_supr₂