Commit 2023-12-09 02:01 5d4fa550

View on Github →

chore(Calculus/Inverse): split (#8603)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Calculus/FDeriv/Equiv.lean

Modified Mathlib/Analysis/Calculus/FDeriv/Mul.lean

Modified Mathlib/Analysis/Calculus/Implicit.lean

Renamed Mathlib/Analysis/Calculus/Inverse.lean to Mathlib/Analysis/Calculus/InverseFunctionTheorem/ApproximatesLinearOn.lean

deleted theorem ApproximatesLinearOn.exists_homeomorph_extension

deleted theorem ContDiffAt.image_mem_toLocalHomeomorph_target

deleted def ContDiffAt.localInverse

deleted theorem ContDiffAt.localInverse_apply_image

deleted theorem ContDiffAt.mem_toLocalHomeomorph_source

deleted def ContDiffAt.toLocalHomeomorph

deleted theorem ContDiffAt.toLocalHomeomorph_coe

deleted theorem ContDiffAt.to_localInverse

deleted def HasStrictDerivAt.localInverse

deleted theorem HasStrictDerivAt.map_nhds_eq

deleted theorem HasStrictDerivAt.to_localInverse

deleted theorem HasStrictDerivAt.to_local_left_inverse

deleted theorem HasStrictFDerivAt.approximates_deriv_on_nhds

deleted theorem HasStrictFDerivAt.approximates_deriv_on_open_nhds

deleted theorem HasStrictFDerivAt.eventually_left_inverse

deleted theorem HasStrictFDerivAt.eventually_right_inverse

deleted theorem HasStrictFDerivAt.image_mem_toLocalHomeomorph_target

deleted def HasStrictFDerivAt.localInverse

deleted theorem HasStrictFDerivAt.localInverse_apply_image

deleted theorem HasStrictFDerivAt.localInverse_continuousAt

deleted theorem HasStrictFDerivAt.localInverse_def

deleted theorem HasStrictFDerivAt.localInverse_tendsto

deleted theorem HasStrictFDerivAt.localInverse_unique

deleted theorem HasStrictFDerivAt.map_nhds_eq_of_equiv

deleted theorem HasStrictFDerivAt.map_nhds_eq_of_surj

deleted theorem HasStrictFDerivAt.mem_toLocalHomeomorph_source

deleted def HasStrictFDerivAt.toLocalHomeomorph

deleted theorem HasStrictFDerivAt.toLocalHomeomorph_coe

deleted theorem HasStrictFDerivAt.to_localInverse

deleted theorem HasStrictFDerivAt.to_local_left_inverse

deleted theorem open_map_of_strict_deriv

deleted theorem open_map_of_strict_fderiv_equiv

Created Mathlib/Analysis/Calculus/InverseFunctionTheorem/ContDiff.lean

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

Created Mathlib/Analysis/Calculus/InverseFunctionTheorem/Deriv.lean

added def HasStrictDerivAt.localInverse

added theorem HasStrictDerivAt.map_nhds_eq

added theorem HasStrictDerivAt.to_localInverse

added theorem HasStrictDerivAt.to_local_left_inverse

added theorem open_map_of_strict_deriv

Created Mathlib/Analysis/Calculus/InverseFunctionTheorem/FDeriv.lean

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 open_map_of_strict_fderiv_equiv

Created Mathlib/Analysis/Calculus/InverseFunctionTheorem/FiniteDimensional.lean

added theorem ApproximatesLinearOn.exists_homeomorph_extension

Modified Mathlib/Analysis/Calculus/LagrangeMultipliers.lean

Modified Mathlib/Analysis/SpecialFunctions/Complex/LogDeriv.lean

Modified Mathlib/MeasureTheory/Function/Jacobian.lean