Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-19 09:54 91b33017

View on Github →

feat(geometry/manifold/cont_mdiff): add various properties (#16980)

  • More lemmas about smooth, more basic lemmas, and some interactions with cont_diff and continuous linear maps
  • Also add various useful lemmas throughout the manifold directory
  • Add me as author to two files (in local_invariant_properties for earlier refactoring PRs)
  • From the sphere eversion project

Estimated changes

added theorem mem_achart_source
added theorem cont_mdiff.clm_comp
added theorem cont_mdiff.fst
added theorem cont_mdiff.snd
added theorem cont_mdiff_at.clm_comp
added theorem cont_mdiff_at.fst
added theorem cont_mdiff_at.snd
added theorem smooth.comp
added theorem smooth.fst
added theorem smooth.snd
added theorem smooth_at.comp
added theorem smooth_at.fst
added theorem smooth_at.snd
added theorem smooth_on.comp'
added theorem smooth_on.comp
added theorem smooth_prod_assoc
added theorem smooth_within_at.comp'
added theorem smooth_within_at.comp
added theorem ext_chart_at_prod