Commit 2024-10-08 22:51 91bc9bf8

View on Github →

chore(ContinuousMap/Defs): extract from Basic (#17265) Move the definition of ContinuousMap to a new file that doesn't depend on Homeomorph, Separation etc Also use X/Y instead of α/β for type vars in the new file.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean

Modified Mathlib/Topology/Algebra/ContinuousAffineMap.lean

Modified Mathlib/Topology/Algebra/Module/Basic.lean

Modified Mathlib/Topology/Algebra/Monoid.lean

Modified Mathlib/Topology/Algebra/Star.lean

Modified Mathlib/Topology/Category/TopCat/Basic.lean

Modified Mathlib/Topology/ContinuousMap/Basic.lean

deleted def ContinuousMap.Simps.apply

deleted theorem ContinuousMap.coe_copy

deleted theorem ContinuousMap.coe_injective

deleted theorem ContinuousMap.coe_mk

deleted theorem ContinuousMap.continuous_set_coe

deleted theorem ContinuousMap.copy_eq

deleted theorem ContinuousMap.ext

deleted theorem ContinuousMap.toFun_eq_coe

deleted structure ContinuousMap

deleted def toContinuousMap

Modified Mathlib/Topology/ContinuousMap/CompactlySupported.lean

Created Mathlib/Topology/ContinuousMap/Defs.lean

added def ContinuousMap.Simps.apply

added theorem ContinuousMap.coe_copy

added theorem ContinuousMap.coe_injective

added theorem ContinuousMap.coe_mk

added theorem ContinuousMap.continuous_set_coe

added theorem ContinuousMap.copy_eq

added theorem ContinuousMap.ext

added theorem ContinuousMap.toFun_eq_coe

added structure ContinuousMap

added def toContinuousMap

Modified Mathlib/Topology/ContinuousMap/Ordered.lean

Modified Mathlib/Topology/ContinuousMap/Sigma.lean

Modified Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean

Modified Mathlib/Topology/Gluing.lean

Modified Mathlib/Topology/Instances/NNReal.lean

Modified Mathlib/Topology/Order/Hom/Basic.lean

Modified Mathlib/Topology/Specialization.lean