Commit 2026-04-11 09:33 15e19695

View on Github →

chore(Order/GaloisConnection/Basic): use to_dual (#37885) This PR uses to_dual for material on GaloisConnection and GaloisInsertion/GaloisCoinsertion. In particular, the instance lifting constructions on GaloisCoinsertion now do not anymore abuse defeq of OrderDual, meaning that we should be able to remove some more backward.isDefEq.respectTransparency.

Estimated changes

deleted theorem GaloisCoinsertion.u_inf_l
deleted theorem GaloisCoinsertion.u_sup_l
deleted theorem GaloisConnection.isLUB_u
modified theorem GaloisConnection.l_iSup
modified theorem GaloisConnection.l_iSup₂
deleted theorem GaloisConnection.u_iInf
deleted theorem GaloisConnection.u_inf
deleted theorem GaloisConnection.u_sInf
deleted theorem OrderIso.bddBelow_image
deleted theorem sInf_image2_eq_sInf_sInf
deleted theorem sInf_image2_eq_sInf_sSup
deleted theorem sInf_image2_eq_sSup_sInf
deleted theorem sInf_image2_eq_sSup_sSup