Commit 2023-06-04 17:52 6ab2e35e

View on Github →

feat: port Analysis.Calculus.Inverse (#4644)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Calculus/Inverse.lean

added theorem ApproximatesLinearOn.approximatesLinearOn_iff_lipschitzOnWith

added theorem ApproximatesLinearOn.closedBall_subset_target

added theorem ApproximatesLinearOn.exists_homeomorph_extension

added theorem ApproximatesLinearOn.image_mem_nhds

added theorem ApproximatesLinearOn.inverse_continuousOn

added theorem ApproximatesLinearOn.lipschitz_sub

added theorem ApproximatesLinearOn.map_nhds_eq

added theorem ApproximatesLinearOn.mono_num

added theorem ApproximatesLinearOn.mono_set

added theorem ApproximatesLinearOn.open_image

added theorem ApproximatesLinearOn.surjOn_closedBall_of_nonlinearRightInverse

added def ApproximatesLinearOn.toHomeomorph

added def ApproximatesLinearOn.toLocalEquiv

added def ApproximatesLinearOn.toLocalHomeomorph

added theorem ApproximatesLinearOn.toLocalHomeomorph_coe

added theorem ApproximatesLinearOn.toLocalHomeomorph_source

added theorem ApproximatesLinearOn.toLocalHomeomorph_target

added theorem ApproximatesLinearOn.to_inv

added def ApproximatesLinearOn

added theorem ContDiffAt.image_mem_toLocalHomeomorph_target

added def ContDiffAt.localInverse

added theorem ContDiffAt.localInverse_apply_image

added theorem ContDiffAt.mem_toLocalHomeomorph_source

added def ContDiffAt.toLocalHomeomorph

added theorem ContDiffAt.toLocalHomeomorph_coe

added theorem ContDiffAt.to_localInverse

added def HasStrictDerivAt.localInverse

added theorem HasStrictDerivAt.map_nhds_eq

added theorem HasStrictDerivAt.to_localInverse

added theorem HasStrictDerivAt.to_local_left_inverse

added theorem HasStrictFDerivAt.approximates_deriv_on_nhds

added theorem HasStrictFDerivAt.approximates_deriv_on_open_nhds

added theorem HasStrictFDerivAt.eventually_left_inverse

added theorem HasStrictFDerivAt.eventually_right_inverse

added theorem HasStrictFDerivAt.image_mem_toLocalHomeomorph_target

added def HasStrictFDerivAt.localInverse

added theorem HasStrictFDerivAt.localInverse_apply_image

added theorem HasStrictFDerivAt.localInverse_continuousAt

added theorem HasStrictFDerivAt.localInverse_def

added theorem HasStrictFDerivAt.localInverse_tendsto

added theorem HasStrictFDerivAt.localInverse_unique

added theorem HasStrictFDerivAt.map_nhds_eq_of_equiv

added theorem HasStrictFDerivAt.map_nhds_eq_of_surj

added theorem HasStrictFDerivAt.mem_toLocalHomeomorph_source

added def HasStrictFDerivAt.toLocalHomeomorph

added theorem HasStrictFDerivAt.toLocalHomeomorph_coe

added theorem HasStrictFDerivAt.to_localInverse

added theorem HasStrictFDerivAt.to_local_left_inverse

added theorem approximatesLinearOn_empty

added theorem open_map_of_strict_deriv

added theorem open_map_of_strict_fderiv_equiv