Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-15 12:40 90db6fcc

View on Github →

feat(analysis/calculus/times_cont_diff): smoothness of f : E → Π i, F i (#6674) Also add helper lemmas/definitions about multilinear maps.

Estimated changes

Modified src/analysis/calculus/times_cont_diff.lean

added theorem has_ftaylor_series_up_to_on_pi'

added theorem has_ftaylor_series_up_to_on_pi

added theorem times_cont_diff_at_pi

added theorem times_cont_diff_on_pi

added theorem times_cont_diff_pi

added theorem times_cont_diff_within_at_pi

Modified src/analysis/normed_space/multilinear.lean

added theorem continuous_multilinear_map.norm_pi

added def continuous_multilinear_map.piₗᵢ

Modified src/geometry/manifold/times_cont_mdiff.lean

added theorem smooth_at_pi_space

added theorem smooth_on_pi_space

added theorem smooth_pi_space

added theorem smooth_within_at_pi_space

added theorem times_cont_mdiff_at_pi_space

added theorem times_cont_mdiff_on_pi_space

added theorem times_cont_mdiff_pi_space

added theorem times_cont_mdiff_within_at_pi_space

Modified src/linear_algebra/multilinear.lean

added def multilinear_map.pi

Modified src/topology/algebra/multilinear.lean

added theorem continuous_multilinear_map.coe_pi

added def continuous_multilinear_map.pi

added theorem continuous_multilinear_map.pi_apply