Commit 2022-12-28 09:54 48d02728

View on Github →

feat: port Order.OrdContinuous (#1241) A few of the fixes I did to get stuff compiling didn't seem correct. Otherwise fine.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/OrdContinuous.lean

added theorem LeftOrdContinuous.coe_toOrderEmbedding

added theorem LeftOrdContinuous.comp

added theorem LeftOrdContinuous.le_iff

added theorem LeftOrdContinuous.lt_iff

added theorem LeftOrdContinuous.map_csupᵢ

added theorem LeftOrdContinuous.map_csupₛ

added theorem LeftOrdContinuous.map_is_greatest

added theorem LeftOrdContinuous.map_sup

added theorem LeftOrdContinuous.map_supᵢ

added theorem LeftOrdContinuous.map_supₛ'

added theorem LeftOrdContinuous.map_supₛ

added theorem LeftOrdContinuous.mono

added def LeftOrdContinuous.toOrderEmbedding

added def LeftOrdContinuous

added theorem RightOrdContinuous.coe_toOrderEmbedding

added theorem RightOrdContinuous.comp

added theorem RightOrdContinuous.le_iff

added theorem RightOrdContinuous.lt_iff

added theorem RightOrdContinuous.map_cinfᵢ

added theorem RightOrdContinuous.map_cinfₛ

added theorem RightOrdContinuous.map_inf

added theorem RightOrdContinuous.map_infᵢ

added theorem RightOrdContinuous.map_infₛ'

added theorem RightOrdContinuous.map_infₛ

added theorem RightOrdContinuous.map_is_least

added theorem RightOrdContinuous.mono

added def RightOrdContinuous.toOrderEmbedding

added def RightOrdContinuous