Commit 2026-04-09 17:17 1147cc38

View on Github →

chore(Order/OrdContinuous): dualize (#37772) Implement all the RightOrdContinuous functionality by dualizing the LeftOrdContinuous versions.

Estimated changes

Modified Mathlib/Order/ConditionallyCompleteLattice/Basic.lean

deleted theorem IsGLB.csInf_eq

deleted theorem isGLB_csInf

Modified Mathlib/Order/OrdContinuous.lean

deleted theorem RightOrdContinuous.coe_toOrderEmbedding

deleted theorem RightOrdContinuous.comp

deleted theorem RightOrdContinuous.le_iff

deleted theorem RightOrdContinuous.lt_iff

deleted theorem RightOrdContinuous.map_ciInf

deleted theorem RightOrdContinuous.map_csInf

deleted theorem RightOrdContinuous.map_iInf

deleted theorem RightOrdContinuous.map_inf

deleted theorem RightOrdContinuous.map_isLeast

deleted theorem RightOrdContinuous.map_sInf'

deleted theorem RightOrdContinuous.map_sInf

deleted theorem RightOrdContinuous.mono

deleted def RightOrdContinuous.toOrderEmbedding

deleted def RightOrdContinuous

Modified Mathlib/Tactic/Translate/ToDual.lean

Modified Mathlib/Topology/Order/Basic.lean