Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-28 22:54 13f30e53

View on Github →

feat(geometry/manifold): ext_chart_at is smooth on its source (#6473)

Estimated changes

Modified src/analysis/calculus/times_cont_diff.lean

added theorem times_cont_diff_within_at.congr'

Modified src/geometry/manifold/smooth_manifold_with_corners.lean

modified theorem ext_chart_at_coe

modified theorem ext_chart_at_coe_symm

added theorem ext_chart_at_continuous_at'

modified theorem ext_chart_at_continuous_at

added theorem ext_chart_at_map_nhds'

added theorem ext_chart_at_map_nhds

added theorem ext_chart_at_source_mem_nhds'

added theorem ext_chart_at_target_subset_range

added theorem ext_chart_continuous_at_symm''

added theorem ext_chart_continuous_on_symm

Modified src/geometry/manifold/times_cont_mdiff.lean

added theorem times_cont_mdiff_at_ext_chart_at'

added theorem times_cont_mdiff_at_ext_chart_at

added theorem times_cont_mdiff_within_at_iff'