Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-04-28 19:57 c435b1cb

View on Github →

feat(analysis/calculus/inverse): Inverse function theorem (#2228) Ref #1849

Estimated changes

Modified src/analysis/asymptotics.lean

added theorem asymptotics.is_o.def'

added theorem asymptotics.is_o.right_is_O_add

added theorem asymptotics.is_o.right_is_O_sub

Modified src/analysis/calculus/deriv.lean

added theorem has_deriv_at.has_fderiv_at_equiv

added theorem has_deriv_at.of_local_left_inverse

added theorem has_strict_deriv_at.has_strict_fderiv_at_equiv

added theorem has_strict_deriv_at.of_local_left_inverse

Modified src/analysis/calculus/fderiv.lean

added theorem has_fderiv_at.of_local_left_inverse

added theorem has_fderiv_at_filter.is_O_sub_rev

deleted theorem has_strict_fderiv_at.comp

deleted theorem has_strict_fderiv_at.continuous_at

deleted theorem has_strict_fderiv_at.differentiable_at

deleted theorem has_strict_fderiv_at.has_fderiv_at

added theorem has_strict_fderiv_at.is_O_sub_rev

added theorem has_strict_fderiv_at.of_local_left_inverse

deleted theorem has_strict_fderiv_at.prod

Created src/analysis/calculus/inverse.lean

added theorem approximates_linear_on.closed_ball_subset_target

added def approximates_linear_on.inverse_approx_map

added theorem approximates_linear_on.inverse_approx_map_contracts_on

added theorem approximates_linear_on.inverse_approx_map_dist_self

added theorem approximates_linear_on.inverse_approx_map_dist_self_le

added theorem approximates_linear_on.inverse_approx_map_fixed_iff

added theorem approximates_linear_on.inverse_approx_map_maps_to

added theorem approximates_linear_on.inverse_approx_map_sub

added theorem approximates_linear_on.inverse_continuous_on

added theorem approximates_linear_on.lipschitz_sub

added theorem approximates_linear_on.mono_num

added theorem approximates_linear_on.mono_set

added theorem approximates_linear_on.surj_on_closed_ball

added def approximates_linear_on.to_local_equiv

added def approximates_linear_on.to_local_homeomorph

added theorem approximates_linear_on.to_local_homeomorph_source

added theorem approximates_linear_on.to_local_homeomorph_target

added theorem approximates_linear_on.to_local_homeomorph_to_fun

added def approximates_linear_on

added def has_strict_deriv_at.local_inverse

added theorem has_strict_deriv_at.to_local_inverse

added theorem has_strict_deriv_at.to_local_left_inverse

added theorem has_strict_fderiv_at.approximates_deriv_on_nhds

added theorem has_strict_fderiv_at.approximates_deriv_on_open_nhds

added theorem has_strict_fderiv_at.eventually_left_inverse

added theorem has_strict_fderiv_at.eventually_right_inverse

added theorem has_strict_fderiv_at.image_mem_to_local_homeomorph_target

added def has_strict_fderiv_at.local_inverse

added theorem has_strict_fderiv_at.local_inverse_apply_image

added theorem has_strict_fderiv_at.local_inverse_continuous_at

added theorem has_strict_fderiv_at.mem_to_local_homeomorph_source

added def has_strict_fderiv_at.to_local_homeomorph

added theorem has_strict_fderiv_at.to_local_homeomorph_to_fun

added theorem has_strict_fderiv_at.to_local_inverse

added theorem has_strict_fderiv_at.to_local_left_inverse

Modified src/analysis/complex/exponential.lean

added theorem real.has_deriv_at_log

Modified src/analysis/normed_space/operator_norm.lean

added theorem continuous_linear_equiv.is_O_comp

added theorem continuous_linear_equiv.is_O_comp_rev

added theorem continuous_linear_equiv.is_O_sub

added theorem continuous_linear_equiv.is_O_sub_rev

Modified src/topology/local_homeomorph.lean

added theorem local_homeomorph.inv_fun_tendsto

Modified src/topology/metric_space/antilipschitz.lean