Commit 2022-02-02 07:21 a18680a6

View on Github →

chore(topology/continuous_function/ordered): split from continuous_function/basic (#11761) Split material about orders out from continuous_function/basic, to move that file lower down the import hierarchy.

Estimated changes

Modified src/combinatorics/configuration.lean

Modified src/topology/continuous_function/algebra.lean

Modified src/topology/continuous_function/basic.lean

deleted def continuous_map.Icc_extend

deleted def continuous_map.abs

deleted theorem continuous_map.abs_apply

deleted theorem continuous_map.coe_Icc_extend

deleted theorem continuous_map.inf'_apply

deleted theorem continuous_map.inf'_coe

deleted theorem continuous_map.inf_apply

deleted theorem continuous_map.inf_coe

deleted theorem continuous_map.le_def

deleted theorem continuous_map.lt_def

deleted theorem continuous_map.sup'_apply

deleted theorem continuous_map.sup'_coe

deleted theorem continuous_map.sup_apply

deleted theorem continuous_map.sup_coe

Created src/topology/continuous_function/ordered.lean

added def continuous_map.Icc_extend

added def continuous_map.abs

added theorem continuous_map.abs_apply

added theorem continuous_map.coe_Icc_extend

added theorem continuous_map.inf'_apply

added theorem continuous_map.inf'_coe

added theorem continuous_map.inf_apply

added theorem continuous_map.inf_coe

added theorem continuous_map.le_def

added theorem continuous_map.lt_def

added theorem continuous_map.sup'_apply

added theorem continuous_map.sup'_coe

added theorem continuous_map.sup_apply

added theorem continuous_map.sup_coe

Modified src/topology/homotopy/basic.lean