Commit 2024-11-28 15:29 0b0b3f79

View on Github →

feat: the pullback of a vector field in a vector space (#19357) We prove notably that the pullback commutes with the Lie bracket.

Estimated changes

Modified Mathlib/Analysis/Calculus/VectorField.lean

added theorem VectorField.DifferentiableWithinAt.pullbackWithin

added theorem VectorField.fderivWithin_pullbackWithin

added theorem VectorField.fderiv_pullback

added def VectorField.pullback

added def VectorField.pullbackWithin

added theorem VectorField.pullbackWithin_eq

added theorem VectorField.pullbackWithin_eq_of_fderivWithin_eq

added theorem VectorField.pullbackWithin_eq_of_not_isInvertible

added theorem VectorField.pullbackWithin_lieBracketWithin_of_isSymmSndFDerivWithinAt

added theorem VectorField.pullbackWithin_lieBracketWithin_of_isSymmSndFDerivWithinAt_of_eventuallyEq

added theorem VectorField.pullbackWithin_univ

added theorem VectorField.pullback_eq_of_fderiv_eq

added theorem VectorField.pullback_eq_of_not_isInvertible

added theorem VectorField.pullback_lieBracket_of_isSymmSndFDerivAt

added theorem exists_continuousLinearEquiv_fderivWithin_symm_eq

added theorem exists_continuousLinearEquiv_fderiv_symm_eq