Commit 2026-03-23 07:35 0bb9155b

View on Github →

chore(Order/Hom/BoundedLattice): use to_dual (#36356)

Estimated changes

Modified Mathlib/Order/Hom/BoundedLattice.lean

deleted theorem BoundedLatticeHom.coe_comp_inf_hom'

deleted theorem BoundedLatticeHom.coe_comp_inf_hom

deleted theorem BoundedLatticeHom.coe_toInfTopHom

modified theorem BoundedLatticeHom.coe_toSupBotHom

deleted def BoundedLatticeHom.toInfTopHom

deleted def BoundedLatticeHom.toSupBotHom

deleted theorem Codisjoint.map

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 def InfTopHom.subtypeVal

deleted theorem InfTopHom.subtypeVal_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

modified structure InfTopHom

modified theorem SupBotHom.coe_mk

modified theorem SupBotHom.coe_toBotHom

modified theorem SupBotHom.coe_toSupHom

modified theorem SupBotHom.comp_id

modified theorem SupBotHom.dual_id

modified theorem SupBotHom.id_comp

deleted def SupBotHom.toBotHom

modified structure SupBotHom