Commit 2021-02-15 13:26 d6db0386

View on Github →

refactor(analysis/normed_space/multilinear): use ≃ₗᵢ for curry equivs (#6232) Also copy some continuous_linear_equiv API to linear_isometry_equiv (e.g., all API in analysis.calculus.fderiv).

Estimated changes

Modified src/analysis/analytic/inverse.lean

Modified src/analysis/analytic/linear.lean

Modified src/analysis/calculus/fderiv.lean

modified theorem continuous_linear_equiv.comp_differentiable_at_iff

modified theorem continuous_linear_equiv.comp_differentiable_iff

modified theorem continuous_linear_equiv.comp_differentiable_on_iff

modified theorem continuous_linear_equiv.comp_differentiable_within_at_iff

modified theorem continuous_linear_equiv.comp_fderiv

modified theorem continuous_linear_equiv.comp_fderiv_within

modified theorem continuous_linear_equiv.comp_has_fderiv_at_iff'

modified theorem continuous_linear_equiv.comp_has_fderiv_at_iff

modified theorem continuous_linear_equiv.comp_has_fderiv_within_at_iff'

modified theorem continuous_linear_equiv.comp_has_fderiv_within_at_iff

modified theorem continuous_linear_equiv.comp_has_strict_fderiv_at_iff

added theorem linear_isometry_equiv.comp_differentiable_at_iff

added theorem linear_isometry_equiv.comp_differentiable_iff

added theorem linear_isometry_equiv.comp_differentiable_on_iff

added theorem linear_isometry_equiv.comp_differentiable_within_at_iff

added theorem linear_isometry_equiv.comp_fderiv

added theorem linear_isometry_equiv.comp_fderiv_within

added theorem linear_isometry_equiv.comp_has_fderiv_at_iff'

added theorem linear_isometry_equiv.comp_has_fderiv_at_iff

added theorem linear_isometry_equiv.comp_has_fderiv_within_at_iff'

added theorem linear_isometry_equiv.comp_has_fderiv_within_at_iff

added theorem linear_isometry_equiv.comp_has_strict_fderiv_at_iff

Modified src/analysis/calculus/times_cont_diff.lean

added theorem continuous_linear_equiv.times_cont_diff

added theorem linear_isometry_equiv.times_cont_diff

added theorem linear_isometry_map.times_cont_diff

Modified src/analysis/normed_space/basic.lean

deleted theorem coe_norm

added theorem submodule.norm_coe

added theorem submodule.norm_mk

Modified src/analysis/normed_space/inner_product.lean

Modified src/analysis/normed_space/linear_isometry.lean

added theorem linear_isometry_equiv.coe_coe''

added theorem linear_isometry_equiv.coe_coe'

added theorem linear_isometry_equiv.coe_coe

deleted theorem linear_isometry_equiv.coe_symm_to_linear_equiv

added theorem linear_isometry_equiv.coe_to_homeomorph

added theorem linear_isometry_equiv.coe_to_isometric

added theorem linear_isometry_equiv.comp_continuous_iff

added theorem linear_isometry_equiv.comp_continuous_on_iff

modified theorem linear_isometry_equiv.diam_image

modified theorem linear_isometry_equiv.ediam_image

modified theorem linear_isometry_equiv.map_eq_iff

deleted def linear_isometry_equiv.to_continuous_linear_equiv

added def linear_isometry_equiv.to_homeomorph

added theorem linear_isometry_equiv.to_homeomorph_symm

added theorem linear_isometry_equiv.to_isometric_symm

added theorem linear_isometry_equiv.to_linear_equiv_symm

Modified src/analysis/normed_space/multilinear.lean

modified def continuous_multilinear_curry_fin0

deleted theorem continuous_multilinear_curry_fin0_apply_norm

deleted def continuous_multilinear_curry_fin0_aux

deleted theorem continuous_multilinear_curry_fin0_symm_apply_norm

modified def continuous_multilinear_curry_fin1

deleted theorem continuous_multilinear_curry_fin1_apply_norm

deleted theorem continuous_multilinear_curry_fin1_symm_apply_norm

deleted def continuous_multilinear_curry_left_equiv_aux

deleted theorem continuous_multilinear_curry_right_equiv_apply_norm

deleted def continuous_multilinear_curry_right_equiv_aux

deleted theorem continuous_multilinear_curry_right_equiv_symm_apply_norm

modified theorem continuous_multilinear_map.curry0_norm

modified theorem continuous_multilinear_map.uncurry0_norm

Modified src/geometry/manifold/instances/sphere.lean

Modified src/topology/algebra/module.lean

modified def continuous_linear_equiv.to_homeomorph

Modified src/topology/metric_space/isometry.lean

added theorem isometry.comp_continuous_iff

added theorem isometry.comp_continuous_on_iff