Commit 2023-02-06 02:37 1f694782

View on Github →

feat: port Topology.ContinuousFunction.Basic (#2053)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/ContinuousFunction/Basic.lean

added theorem ContinuousMap.cancel_left

added theorem ContinuousMap.cancel_right

added theorem ContinuousMap.coe_comp

added theorem ContinuousMap.coe_const

added theorem ContinuousMap.coe_copy

added theorem ContinuousMap.coe_id

added theorem ContinuousMap.coe_injective

added theorem ContinuousMap.coe_mk

added theorem ContinuousMap.coe_restrict

added def ContinuousMap.comp

added theorem ContinuousMap.comp_apply

added theorem ContinuousMap.comp_assoc

added theorem ContinuousMap.comp_const

added theorem ContinuousMap.comp_id

added def ContinuousMap.const

added theorem ContinuousMap.const_apply

added theorem ContinuousMap.const_comp

added theorem ContinuousMap.continuous_set_coe

added theorem ContinuousMap.copy_eq

added def ContinuousMap.equivFnOfDiscrete

added theorem ContinuousMap.ext

added theorem ContinuousMap.id_apply

added theorem ContinuousMap.id_comp

added theorem ContinuousMap.liftCover_coe'

added theorem ContinuousMap.liftCover_coe

added theorem ContinuousMap.liftCover_restrict'

added theorem ContinuousMap.liftCover_restrict

added theorem ContinuousMap.map_specializes

added def ContinuousMap.pi

added theorem ContinuousMap.pi_eval

added def ContinuousMap.prodMap

added def ContinuousMap.prodMk

added theorem ContinuousMap.prod_eval

added def ContinuousMap.restrict

added def ContinuousMap.restrictPreimage

added theorem ContinuousMap.toFun_eq_coe

added structure ContinuousMap

added theorem Homeomorph.coe_refl

added theorem Homeomorph.coe_trans

added theorem Homeomorph.symm_comp_to_continuousMap

added def Homeomorph.toContinuousMap

added theorem Homeomorph.to_continuousMap_comp_symm

added theorem map_continuousAt

added theorem map_continuousWithinAt