Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-17 20:29 75f33464

View on Github →

feat(analysis/normed_space/multilinear): generalized curry (#6270)

Estimated changes

Modified src/analysis/normed_space/multilinear.lean

added def continuous_multilinear_map.curry_fin_finset

added theorem continuous_multilinear_map.curry_fin_finset_apply

added theorem continuous_multilinear_map.curry_fin_finset_apply_const

added theorem continuous_multilinear_map.curry_fin_finset_symm_apply

added theorem continuous_multilinear_map.curry_fin_finset_symm_apply_const

added theorem continuous_multilinear_map.curry_fin_finset_symm_apply_piecewise_const

added def continuous_multilinear_map.curry_sum

added theorem continuous_multilinear_map.curry_sum_apply

added def continuous_multilinear_map.curry_sum_equiv

added def continuous_multilinear_map.dom_dom_congr

added theorem continuous_multilinear_map.le_of_op_norm_le

added def continuous_multilinear_map.uncurry_sum

added theorem continuous_multilinear_map.uncurry_sum_apply

added def multilinear_map.mk_continuous_linear

added theorem multilinear_map.mk_continuous_linear_norm_le'

added theorem multilinear_map.mk_continuous_linear_norm_le

added def multilinear_map.mk_continuous_multilinear

added theorem multilinear_map.mk_continuous_multilinear_apply

added theorem multilinear_map.mk_continuous_multilinear_norm_le'

added theorem multilinear_map.mk_continuous_multilinear_norm_le

added theorem multilinear_map.mk_continuous_norm_le'