Commit 2023-02-06 09:19 604e397d

View on Github →

feat: port Order.Hom.CompleteLattice (#2054) Lot of dangerous instances that were tamed with replacements à la [CompleteLattice x] -> {_ : CompleteLattice x}. Surprisingly smoothly otherwise, perhaps the translation of Sup_hom into SupₛHom is controversial.

Estimated changes

added theorem CompleteLatticeHom.ext
added structure CompleteLatticeHom
added theorem FrameHom.cancel_left
added theorem FrameHom.cancel_right
added theorem FrameHom.coe_comp
added theorem FrameHom.coe_copy
added theorem FrameHom.coe_id
added def FrameHom.comp
added theorem FrameHom.comp_apply
added theorem FrameHom.comp_assoc
added theorem FrameHom.comp_id
added theorem FrameHom.copy_eq
added theorem FrameHom.ext
added theorem FrameHom.id_apply
added theorem FrameHom.id_comp
added theorem FrameHom.toFun_eq_coe
added structure FrameHom
added theorem InfₛHom.cancel_left
added theorem InfₛHom.cancel_right
added theorem InfₛHom.coe_comp
added theorem InfₛHom.coe_copy
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.copy_eq
added theorem InfₛHom.dual_comp
added theorem InfₛHom.dual_id
added theorem InfₛHom.ext
added theorem InfₛHom.id_apply
added theorem InfₛHom.id_comp
added theorem InfₛHom.symm_dual_id
added theorem InfₛHom.toFun_eq_coe
added theorem InfₛHom.top_apply
added structure InfₛHom
added theorem Set.image_supₛ
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_copy
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.copy_eq
added theorem SupₛHom.dual_comp
added theorem SupₛHom.dual_id
added theorem SupₛHom.ext
added theorem SupₛHom.id_apply
added theorem SupₛHom.id_comp
added theorem SupₛHom.symm_dual_id
added theorem SupₛHom.toFun_eq_coe
added structure SupₛHom
added def infInfₛHom
added theorem infInfₛHom_apply
added theorem map_infᵢ
added theorem map_infᵢ₂
added theorem map_supᵢ
added theorem map_supᵢ₂
added def supSupₛHom
added theorem supSupₛHom_apply