Commit 2023-02-07 04:16 3ab70990

View on Github →

feat: port Topology.ContinuousFunction.CocompactMap (#2130)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/ContinuousFunction/CocompactMap.lean

added theorem CocompactMap.coe_comp

added theorem CocompactMap.coe_copy

added theorem CocompactMap.coe_id

added theorem CocompactMap.coe_mk

added theorem CocompactMap.coe_to_continuous_fun

added def CocompactMap.comp

added theorem CocompactMap.comp_apply

added theorem CocompactMap.comp_assoc

added theorem CocompactMap.comp_id

added theorem CocompactMap.copy_eq

added theorem CocompactMap.ext

added theorem CocompactMap.id_comp

added theorem CocompactMap.isCompact_preimage

added theorem CocompactMap.tendsto_of_forall_preimage

added structure CocompactMap

added def Homeomorph.toCocompactMap