Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-02-28 01:50 4637e5c8

View on Github →

refactor(analysis/calculus/times_cont_diff): massive refactor (#2012)

feat(data/fin): append
Update fin.lean
Update fintype.lean
replace but_last with init
cons and append commute
feat(*/multilinear): better multilinear
docstrings
snoc
fix build
comp_snoc and friends
refactor(analysis/calculus/times_cont_diff): massive refactor
fix docstring
move notation
fix build
linter
linter again
Update src/analysis/calculus/times_cont_diff.lean Co-Authored-By: Scott Morrison scott@tqft.net
Update src/analysis/calculus/times_cont_diff.lean Co-Authored-By: Scott Morrison scott@tqft.net
Update src/analysis/calculus/times_cont_diff.lean Co-Authored-By: Scott Morrison scott@tqft.net
Update src/analysis/calculus/times_cont_diff.lean Co-Authored-By: Scott Morrison scott@tqft.net
Update src/analysis/calculus/times_cont_diff.lean Co-Authored-By: Scott Morrison scott@tqft.net
curryfication -> currying

Estimated changes

Modified src/algebra/ordered_ring.lean

added theorem with_top.add_one_le_of_lt

Modified src/analysis/calculus/times_cont_diff.lean

added theorem continuous_linear_equiv.comp_times_cont_diff_on_iff

added theorem continuous_linear_equiv.times_cont_diff_on_comp_iff

added theorem continuous_linear_map.times_cont_diff

added def formal_multilinear_series.shift

added def formal_multilinear_series.unshift

added def formal_multilinear_series

added def ftaylor_series

added def ftaylor_series_within

added theorem ftaylor_series_within_univ

added theorem has_ftaylor_series_up_to.continuous

added theorem has_ftaylor_series_up_to.differentiable

added theorem has_ftaylor_series_up_to.has_fderiv_at

added theorem has_ftaylor_series_up_to.has_ftaylor_series_up_to_on

added theorem has_ftaylor_series_up_to.of_le

added theorem has_ftaylor_series_up_to.zero_eq'

added structure has_ftaylor_series_up_to

added theorem has_ftaylor_series_up_to_on.comp_continuous_linear_map

added theorem has_ftaylor_series_up_to_on.congr

added theorem has_ftaylor_series_up_to_on.continuous_linear_map_comp

added theorem has_ftaylor_series_up_to_on.continuous_on

added theorem has_ftaylor_series_up_to_on.differentiable_on

added theorem has_ftaylor_series_up_to_on.eq_ftaylor_series_of_unique_diff_on

added theorem has_ftaylor_series_up_to_on.has_fderiv_within_at

added theorem has_ftaylor_series_up_to_on.mono

added theorem has_ftaylor_series_up_to_on.of_le

added theorem has_ftaylor_series_up_to_on.prod

added theorem has_ftaylor_series_up_to_on.zero_eq'

added structure has_ftaylor_series_up_to_on

added theorem has_ftaylor_series_up_to_on_succ_iff_left

added theorem has_ftaylor_series_up_to_on_succ_iff_right

added theorem has_ftaylor_series_up_to_on_top_iff

added theorem has_ftaylor_series_up_to_on_univ_iff

added theorem has_ftaylor_series_up_to_on_zero_iff

added theorem has_ftaylor_series_up_to_succ_iff_right

added theorem has_ftaylor_series_up_to_zero_iff

deleted def iterated_continuous_linear_map.normed_group_rec

deleted def iterated_continuous_linear_map.normed_space_rec

deleted def iterated_continuous_linear_map

deleted def iterated_fderiv

added theorem iterated_fderiv_one_apply

deleted theorem iterated_fderiv_succ

added theorem iterated_fderiv_succ_apply_left

added theorem iterated_fderiv_succ_apply_right

added theorem iterated_fderiv_succ_eq_comp_left

added theorem iterated_fderiv_succ_eq_comp_right

deleted def iterated_fderiv_within

modified theorem iterated_fderiv_within_congr

added theorem iterated_fderiv_within_inter'

modified theorem iterated_fderiv_within_inter

modified theorem iterated_fderiv_within_inter_open

added theorem iterated_fderiv_within_one_apply

deleted theorem iterated_fderiv_within_succ

added theorem iterated_fderiv_within_succ_apply_left

added theorem iterated_fderiv_within_succ_apply_right

added theorem iterated_fderiv_within_succ_eq_comp_left

added theorem iterated_fderiv_within_succ_eq_comp_right

modified theorem iterated_fderiv_within_univ

deleted theorem iterated_fderiv_within_zero

added theorem iterated_fderiv_within_zero_apply

added theorem iterated_fderiv_within_zero_eq_comp

added theorem iterated_fderiv_within_zero_fun

deleted theorem iterated_fderiv_zero

added theorem iterated_fderiv_zero_apply

added theorem iterated_fderiv_zero_eq_comp

added theorem times_cont_diff.comp_continuous_linear_map

deleted theorem times_cont_diff.comp_is_bounded_linear

modified theorem times_cont_diff.continuous

modified theorem times_cont_diff.continuous_fderiv

modified theorem times_cont_diff.continuous_fderiv_apply

added theorem times_cont_diff.continuous_linear_map_comp

added theorem times_cont_diff.differentiable

modified theorem times_cont_diff.of_le

deleted theorem times_cont_diff.of_succ

modified theorem times_cont_diff.times_cont_diff_fderiv_apply

modified theorem times_cont_diff.times_cont_diff_on

deleted def times_cont_diff

added theorem times_cont_diff_iff_continuous_differentiable

deleted theorem times_cont_diff_iff_times_cont_diff_rec

added theorem times_cont_diff_of_differentiable_iterated_fderiv

modified theorem times_cont_diff_on.comp

added theorem times_cont_diff_on.comp_continuous_linear_map

deleted theorem times_cont_diff_on.comp_is_bounded_linear

modified theorem times_cont_diff_on.congr

deleted theorem times_cont_diff_on.congr_mono'

modified theorem times_cont_diff_on.congr_mono

added theorem times_cont_diff_on.continuous_linear_map_comp

modified theorem times_cont_diff_on.continuous_on

modified theorem times_cont_diff_on.continuous_on_fderiv_within

added theorem times_cont_diff_on.continuous_on_iterated_fderiv_within

modified theorem times_cont_diff_on.differentiable_on

added theorem times_cont_diff_on.differentiable_on_iterated_fderiv_within

added theorem times_cont_diff_on.fderiv_within

added theorem times_cont_diff_on.ftaylor_series_within

modified theorem times_cont_diff_on.mono

deleted theorem times_cont_diff_on.of_succ

deleted def times_cont_diff_on

added theorem times_cont_diff_on_congr

modified theorem times_cont_diff_on_const

deleted theorem times_cont_diff_on_fderiv_within

deleted theorem times_cont_diff_on_fderiv_within_nat

added theorem times_cont_diff_on_iff_continuous_on_differentiable_on

added theorem times_cont_diff_on_iff_ftaylor_series

deleted theorem times_cont_diff_on_iff_times_cont_diff_on_rec

added theorem times_cont_diff_on_nat

added theorem times_cont_diff_on_of_continuous_on_differentiable_on

added theorem times_cont_diff_on_of_differentiable_on

modified theorem times_cont_diff_on_of_locally_times_cont_diff_on

deleted theorem times_cont_diff_on_rec.continuous_on_iterated_fderiv_within

deleted theorem times_cont_diff_on_rec.differentiable_on

deleted theorem times_cont_diff_on_rec.of_succ

deleted def times_cont_diff_on_rec

deleted theorem times_cont_diff_on_rec_succ

deleted theorem times_cont_diff_on_rec_univ

deleted theorem times_cont_diff_on_rec_zero

deleted theorem times_cont_diff_on_succ

added theorem times_cont_diff_on_succ_iff_fderiv_within

added theorem times_cont_diff_on_succ_iff_has_fderiv_within_at

added theorem times_cont_diff_on_top_iff_fderiv_within

modified theorem times_cont_diff_on_univ

deleted theorem times_cont_diff_rec.continuous

deleted theorem times_cont_diff_rec.differentiable

deleted theorem times_cont_diff_rec.of_succ

deleted def times_cont_diff_rec

deleted theorem times_cont_diff_rec_succ

deleted theorem times_cont_diff_rec_zero

deleted theorem times_cont_diff_succ

added theorem times_cont_diff_succ_iff_fderiv

modified theorem times_cont_diff_top

added theorem times_cont_diff_top_iff_fderiv

added theorem times_cont_diff_zero_fun

Modified src/analysis/normed_space/bounded_linear_maps.lean

added theorem is_bounded_bilinear_map.is_bounded_linear_map_left

added theorem is_bounded_bilinear_map.is_bounded_linear_map_right

added theorem is_bounded_bilinear_map_comp_multilinear

added theorem is_bounded_linear_map_continuous_multilinear_map_comp_linear

added theorem is_bounded_linear_map_prod_multilinear

Modified src/analysis/normed_space/multilinear.lean

Modified src/geometry/manifold/basic_smooth_bundle.lean

Modified src/geometry/manifold/mfderiv.lean

Modified src/geometry/manifold/real_instances.lean

Modified src/geometry/manifold/smooth_manifold_with_corners.lean

Modified src/linear_algebra/multilinear.lean

Modified src/topology/algebra/multilinear.lean

Modified src/topology/continuous_on.lean

added theorem mem_of_mem_nhds_within