Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-29 17:21 0d18179a

View on Github →

chore(analysis/normed_space/multilinear): rename variables (#5929) Use E and E' for indexed types and G and G' for Type*s.

Estimated changes

Modified src/analysis/normed_space/multilinear.lean

modified def continuous_multilinear_curry_fin0

modified theorem continuous_multilinear_curry_fin0_apply

modified def continuous_multilinear_curry_fin0_aux

modified theorem continuous_multilinear_curry_fin0_symm_apply

modified def continuous_multilinear_curry_fin1

modified theorem continuous_multilinear_curry_fin1_apply

modified theorem continuous_multilinear_map.apply_zero_curry0

modified theorem continuous_multilinear_map.bounds_bdd_below

modified theorem continuous_multilinear_map.bounds_nonempty

modified theorem continuous_multilinear_map.continuous_eval_left

modified def continuous_multilinear_map.curry0

modified theorem continuous_multilinear_map.curry0_apply

modified theorem continuous_multilinear_map.curry0_norm

modified theorem continuous_multilinear_map.curry0_uncurry0

modified theorem continuous_multilinear_map.fin0_apply_norm

modified theorem continuous_multilinear_map.mk_pi_field_apply

modified theorem continuous_multilinear_map.mk_pi_field_apply_one_eq_self

modified theorem continuous_multilinear_map.norm_image_sub_le'

modified theorem continuous_multilinear_map.norm_image_sub_le

modified theorem continuous_multilinear_map.norm_restr

modified def continuous_multilinear_map.restr

modified theorem continuous_multilinear_map.uncurry0_apply

modified theorem continuous_multilinear_map.uncurry0_curry0

modified theorem continuous_multilinear_map.uncurry0_norm

modified theorem multilinear_map.mk_continuous_norm_le

modified theorem multilinear_map.restr_norm_le