Commit 2025-03-25 12:21 6e043440

View on Github →

chore: split Order.Hom.Lattice (#23249) There is now a (good) diamond of files Order.Hom.Basic -> .Bounded, .Lattice -> .BoundedLattice containing the declarations for order maps and lattice homomorphisms. Results on adjoining ⊤ and ⊥ are now in Order.Hom.WithTopBot. The latter file is also populated with WithTop/WithBot-containing declarations from Order.Hom.Basic.

Estimated changes

deleted def WithBot.coeOrderHom
deleted def WithTop.coeOrderHom
added theorem BoundedLatticeHom.ext
added structure BoundedLatticeHom
added theorem Codisjoint.map
added theorem Disjoint.map
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_mk
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_id
added theorem InfTopHom.toFun_eq_coe
added theorem InfTopHom.top_apply
added structure InfTopHom
added theorem IsCompl.map
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_mk
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_id
added theorem SupBotHom.toFun_eq_coe
added structure SupBotHom
added theorem map_compl'
added theorem map_sdiff'
added theorem map_symmDiff'
deleted theorem BoundedLatticeHom.coe_id
deleted theorem BoundedLatticeHom.coe_mk
deleted theorem BoundedLatticeHom.comp_id
deleted theorem BoundedLatticeHom.copy_eq
deleted theorem BoundedLatticeHom.dual_id
deleted theorem BoundedLatticeHom.ext
deleted theorem BoundedLatticeHom.id_comp
deleted structure BoundedLatticeHom
deleted theorem Codisjoint.map
deleted theorem Disjoint.map
deleted def InfHom.withBot'
deleted theorem InfHom.withBot_comp
deleted theorem InfHom.withBot_id
deleted def InfHom.withTop'
deleted theorem InfHom.withTop_comp
deleted theorem InfHom.withTop_id
deleted theorem InfTopHom.cancel_left
deleted theorem InfTopHom.cancel_right
deleted theorem InfTopHom.coe_comp
deleted theorem InfTopHom.coe_copy
deleted theorem InfTopHom.coe_id
deleted theorem InfTopHom.coe_inf
deleted theorem InfTopHom.coe_mk
deleted theorem InfTopHom.coe_toInfHom
deleted theorem InfTopHom.coe_toTopHom
deleted theorem InfTopHom.coe_top
deleted def InfTopHom.comp
deleted theorem InfTopHom.comp_apply
deleted theorem InfTopHom.comp_assoc
deleted theorem InfTopHom.comp_id
deleted theorem InfTopHom.copy_eq
deleted theorem InfTopHom.dual_comp
deleted theorem InfTopHom.dual_id
deleted theorem InfTopHom.ext
deleted theorem InfTopHom.id_apply
deleted theorem InfTopHom.id_comp
deleted theorem InfTopHom.inf_apply
deleted theorem InfTopHom.subtypeVal_coe
deleted theorem InfTopHom.symm_dual_comp
deleted theorem InfTopHom.symm_dual_id
deleted theorem InfTopHom.toFun_eq_coe
deleted def InfTopHom.toTopHom
deleted theorem InfTopHom.top_apply
deleted structure InfTopHom
deleted theorem IsCompl.map
deleted theorem LatticeHom.coe_withBot
deleted theorem LatticeHom.coe_withTop
deleted def LatticeHom.withBot'
deleted theorem LatticeHom.withBot_apply
deleted theorem LatticeHom.withBot_comp
deleted theorem LatticeHom.withBot_id
deleted def LatticeHom.withTop'
deleted theorem LatticeHom.withTop_apply
deleted theorem LatticeHom.withTop_comp
deleted theorem LatticeHom.withTop_id
deleted theorem SupBotHom.bot_apply
deleted theorem SupBotHom.cancel_left
deleted theorem SupBotHom.cancel_right
deleted theorem SupBotHom.coe_bot
deleted theorem SupBotHom.coe_comp
deleted theorem SupBotHom.coe_copy
deleted theorem SupBotHom.coe_id
deleted theorem SupBotHom.coe_mk
deleted theorem SupBotHom.coe_sup
deleted theorem SupBotHom.coe_toBotHom
deleted theorem SupBotHom.coe_toSupHom
deleted def SupBotHom.comp
deleted theorem SupBotHom.comp_apply
deleted theorem SupBotHom.comp_assoc
deleted theorem SupBotHom.comp_id
deleted theorem SupBotHom.copy_eq
deleted def SupBotHom.dual
deleted theorem SupBotHom.dual_comp
deleted theorem SupBotHom.dual_id
deleted theorem SupBotHom.ext
deleted theorem SupBotHom.id_apply
deleted theorem SupBotHom.id_comp
deleted theorem SupBotHom.subtypeVal_coe
deleted theorem SupBotHom.sup_apply
deleted theorem SupBotHom.symm_dual_comp
deleted theorem SupBotHom.symm_dual_id
deleted def SupBotHom.toBotHom
deleted theorem SupBotHom.toFun_eq_coe
deleted structure SupBotHom
deleted def SupHom.withBot'
deleted theorem SupHom.withBot_comp
deleted theorem SupHom.withBot_id
deleted def SupHom.withTop'
deleted theorem SupHom.withTop_comp
deleted theorem SupHom.withTop_id
deleted theorem map_compl'
deleted theorem map_sdiff'
deleted theorem map_symmDiff'
added def InfHom.withBot'
added theorem InfHom.withBot_comp
added theorem InfHom.withBot_id
added def InfHom.withTop'
added theorem InfHom.withTop_comp
added theorem InfHom.withTop_id
added theorem LatticeHom.coe_withBot
added theorem LatticeHom.coe_withTop
added theorem LatticeHom.withBot_id
added theorem LatticeHom.withTop_id
added def SupHom.withBot'
added theorem SupHom.withBot_comp
added theorem SupHom.withBot_id
added def SupHom.withTop'
added theorem SupHom.withTop_comp
added theorem SupHom.withTop_id