Commit 2023-02-22 20:00 ce3bef26

View on Github →

feat: port Topology.ContinuousFunction.Ordered (#2448)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/ContinuousFunction/Ordered.lean

added def ContinuousMap.IccExtend

added def ContinuousMap.abs

added theorem ContinuousMap.abs_apply

added theorem ContinuousMap.coe_IccExtend

added theorem ContinuousMap.inf'_apply

added theorem ContinuousMap.inf'_coe

added theorem ContinuousMap.inf_apply

added theorem ContinuousMap.inf_coe

added theorem ContinuousMap.le_def

added theorem ContinuousMap.lt_def

added theorem ContinuousMap.sup'_apply

added theorem ContinuousMap.sup'_coe

added theorem ContinuousMap.sup_apply

added theorem ContinuousMap.sup_coe