Commit 2023-05-22 19:15 d911e507

View on Github →

feat: port Analysis.Calculus.Fderiv.Equiv (#4210)

Estimated changes

Modified Mathlib.lean

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

added theorem ContinuousLinearEquiv.comp_differentiableAt_iff

added theorem ContinuousLinearEquiv.comp_differentiableOn_iff

added theorem ContinuousLinearEquiv.comp_differentiableWithinAt_iff

added theorem ContinuousLinearEquiv.comp_differentiable_iff

added theorem ContinuousLinearEquiv.comp_fderiv

added theorem ContinuousLinearEquiv.comp_fderivWithin

added theorem ContinuousLinearEquiv.comp_hasFDerivAt_iff'

added theorem ContinuousLinearEquiv.comp_hasFDerivAt_iff

added theorem ContinuousLinearEquiv.comp_hasFDerivWithinAt_iff'

added theorem ContinuousLinearEquiv.comp_hasFDerivWithinAt_iff

added theorem ContinuousLinearEquiv.comp_hasStrictFDerivAt_iff

added theorem ContinuousLinearEquiv.comp_right_differentiableAt_iff

added theorem ContinuousLinearEquiv.comp_right_differentiableOn_iff

added theorem ContinuousLinearEquiv.comp_right_differentiableWithinAt_iff

added theorem ContinuousLinearEquiv.comp_right_differentiable_iff

added theorem ContinuousLinearEquiv.comp_right_fderiv

added theorem ContinuousLinearEquiv.comp_right_fderivWithin

added theorem ContinuousLinearEquiv.comp_right_hasFDerivAt_iff'

added theorem ContinuousLinearEquiv.comp_right_hasFDerivAt_iff

added theorem ContinuousLinearEquiv.comp_right_hasFDerivWithinAt_iff'

added theorem ContinuousLinearEquiv.comp_right_hasFDerivWithinAt_iff

added theorem ContinuousLinearEquiv.uniqueDiffOn_image

added theorem ContinuousLinearEquiv.uniqueDiffOn_image_iff

added theorem ContinuousLinearEquiv.uniqueDiffOn_preimage_iff

added theorem HasFDerivAt.eventually_ne

added theorem HasFDerivAt.lim_real

added theorem HasFDerivAt.of_local_left_inverse

added theorem HasFDerivWithinAt.eventually_ne

added theorem HasFDerivWithinAt.mapsTo_tangent_cone

added theorem HasFDerivWithinAt.uniqueDiffWithinAt

added theorem HasFDerivWithinAt.uniqueDiffWithinAt_of_continuousLinearEquiv

added theorem HasStrictFDerivAt.of_local_left_inverse

added theorem LinearIsometryEquiv.comp_differentiableAt_iff

added theorem LinearIsometryEquiv.comp_differentiableOn_iff

added theorem LinearIsometryEquiv.comp_differentiableWithinAt_iff

added theorem LinearIsometryEquiv.comp_differentiable_iff

added theorem LinearIsometryEquiv.comp_fderiv

added theorem LinearIsometryEquiv.comp_fderivWithin

added theorem LinearIsometryEquiv.comp_hasFDerivAt_iff'

added theorem LinearIsometryEquiv.comp_hasFDerivAt_iff

added theorem LinearIsometryEquiv.comp_hasFDerivWithinAt_iff'

added theorem LinearIsometryEquiv.comp_hasFDerivWithinAt_iff

added theorem LinearIsometryEquiv.comp_hasStrictFDerivAt_iff

added theorem LocalHomeomorph.hasFDerivAt_symm

added theorem LocalHomeomorph.hasStrictFDerivAt_symm

added theorem UniqueDiffOn.image

added theorem has_fderiv_at_filter_real_equiv