Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-23 20:55 9aeffa83

View on Github →

feat(geometry/manifold): bundled smooth map (#3904)

Estimated changes

Modified src/geometry/manifold/smooth_manifold_with_corners.lean

Modified src/geometry/manifold/times_cont_mdiff.lean

added theorem continuous_linear_map.times_cont_mdiff

Created src/geometry/manifold/times_cont_mdiff_map.lean

added def smooth_map

added theorem times_cont_mdiff_map.coe_inj

added def times_cont_mdiff_map.comp

added theorem times_cont_mdiff_map.comp_apply

added def times_cont_mdiff_map.const

added theorem times_cont_mdiff_map.ext

added def times_cont_mdiff_map.id

added structure times_cont_mdiff_map