Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-26 10:40 597946df

View on Github →

feat(analysis/calculus/implicit): Implicit function theorem (#2749) Fixes #1849 Zulip thread.

Estimated changes

Modified src/analysis/calculus/deriv.lean

deleted theorem has_strict_fderiv_at.has_strict_deriv_at

Created src/analysis/calculus/implicit.lean

added theorem has_strict_fderiv_at.eq_implicit_function

added theorem has_strict_fderiv_at.eq_implicit_function_of_complemented

added def has_strict_fderiv_at.implicit_function

added def has_strict_fderiv_at.implicit_function_data_of_complemented

added def has_strict_fderiv_at.implicit_function_of_complemented

added def has_strict_fderiv_at.implicit_to_local_homeomorph

added theorem has_strict_fderiv_at.implicit_to_local_homeomorph_apply_ker

added theorem has_strict_fderiv_at.implicit_to_local_homeomorph_fst

added def has_strict_fderiv_at.implicit_to_local_homeomorph_of_complemented

added theorem has_strict_fderiv_at.implicit_to_local_homeomorph_of_complemented_apply

added theorem has_strict_fderiv_at.implicit_to_local_homeomorph_of_complemented_apply_ker

added theorem has_strict_fderiv_at.implicit_to_local_homeomorph_of_complemented_fst

added theorem has_strict_fderiv_at.implicit_to_local_homeomorph_of_complemented_self

added theorem has_strict_fderiv_at.implicit_to_local_homeomorph_self

added theorem has_strict_fderiv_at.map_implicit_function_eq

added theorem has_strict_fderiv_at.map_implicit_function_of_complemented_eq

added theorem has_strict_fderiv_at.mem_implicit_to_local_homeomorph_of_complemented_source

added theorem has_strict_fderiv_at.mem_implicit_to_local_homeomorph_of_complemented_target

added theorem has_strict_fderiv_at.mem_implicit_to_local_homeomorph_source

added theorem has_strict_fderiv_at.mem_implicit_to_local_homeomorph_target

added theorem has_strict_fderiv_at.to_implicit_function

added theorem has_strict_fderiv_at.to_implicit_function_of_complemented

added def implicit_function_data.implicit_function

added theorem implicit_function_data.implicit_function_apply_image

added theorem implicit_function_data.implicit_function_has_strict_fderiv_at

added theorem implicit_function_data.left_map_implicit_function

added theorem implicit_function_data.map_pt_mem_to_local_homeomorph_target

added def implicit_function_data.prod_fun

added theorem implicit_function_data.prod_fun_apply

added theorem implicit_function_data.prod_map_implicit_function

added theorem implicit_function_data.pt_mem_to_local_homeomorph_source

added theorem implicit_function_data.right_map_implicit_function

added def implicit_function_data.to_local_homeomorph

added theorem implicit_function_data.to_local_homeomorph_apply

added theorem implicit_function_data.to_local_homeomorph_coe

added structure implicit_function_data

Modified src/analysis/normed_space/operator_norm.lean

modified theorem continuous_linear_map.is_O_comp

Modified src/topology/algebra/module.lean

added theorem continuous_linear_map.is_complete_ker