Commit 2026-03-26 22:21 c71f8158

View on Github →

chore(Order/Hom/CompleteLattice): use to_dual (#37035) This PR uses to_dual to translate sSupHom/sInfHom.

Estimated changes

deleted theorem map_iInf
deleted theorem map_iInf₂
modified theorem map_iSup
deleted theorem sInfHom.cancel_left
deleted theorem sInfHom.cancel_right
deleted theorem sInfHom.coe_comp
deleted theorem sInfHom.coe_copy
deleted theorem sInfHom.coe_id
deleted theorem sInfHom.coe_mk
deleted theorem sInfHom.coe_top
deleted def sInfHom.comp
deleted theorem sInfHom.comp_apply
deleted theorem sInfHom.comp_assoc
deleted theorem sInfHom.comp_id
deleted theorem sInfHom.copy_eq
deleted theorem sInfHom.dual_comp
deleted theorem sInfHom.dual_id
deleted theorem sInfHom.ext
deleted theorem sInfHom.id_apply
deleted theorem sInfHom.id_comp
deleted theorem sInfHom.symm_dual_comp
deleted theorem sInfHom.symm_dual_id
deleted theorem sInfHom.toFun_eq_coe
deleted theorem sInfHom.top_apply
modified theorem sSupHom.coe_mk
modified theorem sSupHom.toFun_eq_coe