Commit 2023-02-03 17:54 e7dba9c7

View on Github →

feat: port Order.Hom.Lattice (#1636)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Logic/Equiv/Defs.lean

Created Mathlib/Order/Hom/Lattice.lean

added theorem BoundedLatticeHom.cancel_left

added theorem BoundedLatticeHom.cancel_right

added theorem BoundedLatticeHom.coe_comp

added theorem BoundedLatticeHom.coe_comp_inf_hom'

added theorem BoundedLatticeHom.coe_comp_inf_hom

added theorem BoundedLatticeHom.coe_comp_lattice_hom'

added theorem BoundedLatticeHom.coe_comp_lattice_hom

added theorem BoundedLatticeHom.coe_comp_sup_hom'

added theorem BoundedLatticeHom.coe_comp_sup_hom

added theorem BoundedLatticeHom.coe_copy

added theorem BoundedLatticeHom.coe_id

added theorem BoundedLatticeHom.coe_toLatticeHom

added def BoundedLatticeHom.comp

added theorem BoundedLatticeHom.comp_apply

added theorem BoundedLatticeHom.comp_assoc

added theorem BoundedLatticeHom.comp_id

added theorem BoundedLatticeHom.copy_eq

added theorem BoundedLatticeHom.dual_comp

added theorem BoundedLatticeHom.dual_id

added theorem BoundedLatticeHom.ext

added theorem BoundedLatticeHom.id_apply

added theorem BoundedLatticeHom.id_comp

added theorem BoundedLatticeHom.symm_dual_comp

added theorem BoundedLatticeHom.symm_dual_id

added def BoundedLatticeHom.toBoundedOrderHom

added theorem BoundedLatticeHom.toFun_eq_coe

added def BoundedLatticeHom.toInfTopHom

added def BoundedLatticeHom.toSupBotHom

added structure BoundedLatticeHom

added theorem Codisjoint.map

added theorem Disjoint.map

added theorem InfHom.bot_apply

added theorem InfHom.cancel_left

added theorem InfHom.cancel_right

added theorem InfHom.coe_bot

added theorem InfHom.coe_comp

added theorem InfHom.coe_const

added theorem InfHom.coe_copy

added theorem InfHom.coe_id

added theorem InfHom.coe_inf

added theorem InfHom.coe_top

added def InfHom.comp

added theorem InfHom.comp_apply

added theorem InfHom.comp_assoc

added theorem InfHom.comp_id

added def InfHom.const

added theorem InfHom.const_apply

added theorem InfHom.copy_eq

added theorem InfHom.dual_comp

added theorem InfHom.dual_id

added theorem InfHom.ext

added theorem InfHom.id_apply

added theorem InfHom.id_comp

added theorem InfHom.inf_apply

added theorem InfHom.symm_dual_comp

added theorem InfHom.symm_dual_id

added theorem InfHom.toFun_eq_coe

added theorem InfHom.top_apply

added structure InfHom

added theorem InfTopHom.cancel_left

added theorem InfTopHom.cancel_right

added theorem InfTopHom.coe_comp

added theorem InfTopHom.coe_copy

added theorem InfTopHom.coe_id

added theorem InfTopHom.coe_inf

added theorem InfTopHom.coe_toInfHom

added theorem InfTopHom.coe_toTopHom

added theorem InfTopHom.coe_top

added def InfTopHom.comp

added theorem InfTopHom.comp_apply

added theorem InfTopHom.comp_assoc

added theorem InfTopHom.comp_id

added theorem InfTopHom.copy_eq

added theorem InfTopHom.dual_comp

added theorem InfTopHom.dual_id

added theorem InfTopHom.ext

added theorem InfTopHom.id_apply

added theorem InfTopHom.id_comp

added theorem InfTopHom.inf_apply

added theorem InfTopHom.symm_dual_comp

added theorem InfTopHom.symm_dual_id

added theorem InfTopHom.toFun_eq_coe

added def InfTopHom.toTopHom

added theorem InfTopHom.top_apply

added structure InfTopHom

added theorem IsCompl.map

added theorem LatticeHom.cancel_left

added theorem LatticeHom.cancel_right

added theorem LatticeHom.coe_comp

added theorem LatticeHom.coe_comp_inf_hom'

added theorem LatticeHom.coe_comp_inf_hom

added theorem LatticeHom.coe_comp_sup_hom'

added theorem LatticeHom.coe_comp_sup_hom

added theorem LatticeHom.coe_copy

added theorem LatticeHom.coe_id

added theorem LatticeHom.coe_toInfHom

added theorem LatticeHom.coe_toSupHom

added def LatticeHom.comp

added theorem LatticeHom.comp_apply

added theorem LatticeHom.comp_assoc

added theorem LatticeHom.comp_id

added theorem LatticeHom.copy_eq

added theorem LatticeHom.dual_comp

added theorem LatticeHom.dual_id

added theorem LatticeHom.ext

added theorem LatticeHom.id_apply

added theorem LatticeHom.id_comp

added theorem LatticeHom.symm_dual_comp

added theorem LatticeHom.symm_dual_id

added theorem LatticeHom.toFun_eq_coe

added def LatticeHom.toInfHom

added structure LatticeHom

added theorem OrderHomClass.coe_to_lattice_hom

added def OrderHomClass.toLatticeHom

added theorem OrderHomClass.to_lattice_hom_apply

added theorem SupBotHom.bot_apply

added theorem SupBotHom.cancel_left

added theorem SupBotHom.cancel_right

added theorem SupBotHom.coe_bot

added theorem SupBotHom.coe_comp

added theorem SupBotHom.coe_copy

added theorem SupBotHom.coe_id

added theorem SupBotHom.coe_sup

added theorem SupBotHom.coe_toBotHom

added theorem SupBotHom.coe_toSupHom

added def SupBotHom.comp

added theorem SupBotHom.comp_apply

added theorem SupBotHom.comp_assoc

added theorem SupBotHom.comp_id

added theorem SupBotHom.copy_eq

added def SupBotHom.dual

added theorem SupBotHom.dual_comp

added theorem SupBotHom.dual_id

added theorem SupBotHom.ext

added theorem SupBotHom.id_apply

added theorem SupBotHom.id_comp

added theorem SupBotHom.sup_apply

added theorem SupBotHom.symm_dual_comp

added theorem SupBotHom.symm_dual_id

added def SupBotHom.toBotHom

added theorem SupBotHom.toFun_eq_coe

added structure SupBotHom

added theorem SupHom.bot_apply

added theorem SupHom.cancel_left

added theorem SupHom.cancel_right

added theorem SupHom.coe_bot

added theorem SupHom.coe_comp

added theorem SupHom.coe_const

added theorem SupHom.coe_copy

added theorem SupHom.coe_id

added theorem SupHom.coe_sup

added theorem SupHom.coe_top

added def SupHom.comp

added theorem SupHom.comp_apply

added theorem SupHom.comp_assoc

added theorem SupHom.comp_id

added def SupHom.const

added theorem SupHom.const_apply

added theorem SupHom.copy_eq

added theorem SupHom.dual_comp

added theorem SupHom.dual_id

added theorem SupHom.ext

added theorem SupHom.id_apply

added theorem SupHom.id_comp

added theorem SupHom.sup_apply

added theorem SupHom.symm_dual_comp

added theorem SupHom.symm_dual_id

added theorem SupHom.toFun_eq_coe

added theorem SupHom.top_apply

added structure SupHom

added theorem map_compl'

added theorem map_finset_inf

added theorem map_finset_sup

added theorem map_sdiff'

added theorem map_symm_diff'