Commit 2023-06-24 05:50 83bcf1b9

View on Github →

feat: port Geometry.Manifold.ContMdiffMap (#5436)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Geometry/Manifold/ContMDiffMap.lean

added theorem ContMDiffMap.coeFn_mk

added theorem ContMDiffMap.coe_injective

added def ContMDiffMap.comp

added theorem ContMDiffMap.comp_apply

added def ContMDiffMap.const

added theorem ContMDiffMap.ext

added def ContMDiffMap.fst

added def ContMDiffMap.prodMk

added def ContMDiffMap.snd

added def ContMDiffMap

added def SmoothMap

Modified Mathlib/Topology/ContinuousFunction/Basic.lean

added def toContinuousMap

Modified Mathlib/Topology/ContinuousFunction/Ideals.lean

Modified Mathlib/Topology/ContinuousFunction/ZeroAtInfty.lean