Commit 2024-11-20 14:53 185ec9cd

View on Github →

feat: the Lie bracket of vector fields in vector spaces (#18852)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Calculus/VectorField.lean

added theorem ContDiff.lieBracket_vectorField

added theorem ContDiffAt.lieBracket_vectorField

added theorem ContDiffOn.lieBracketWithin_vectorField

added theorem ContDiffWithinAt.lieBracketWithin_vectorField

added theorem DifferentiableWithinAt.lieBracketWithin_congr_mono

added theorem Filter.EventuallyEq.lieBracketWithin_vectorField'

added theorem Filter.EventuallyEq.lieBracketWithin_vectorField_eq

added theorem Filter.EventuallyEq.lieBracketWithin_vectorField_eq_nhds

added theorem Filter.EventuallyEq.lieBracketWithin_vectorField_eq_of_mem

added theorem Filter.EventuallyEq.lieBracket_vectorField_eq

added theorem VectorField.leibniz_identity_lieBracket

added theorem VectorField.leibniz_identity_lieBracketWithin

added theorem VectorField.leibniz_identity_lieBracketWithin_of_isSymmSndFDerivWithinAt

added def VectorField.lieBracket

added def VectorField.lieBracketWithin

added theorem VectorField.lieBracketWithin_add_left

added theorem VectorField.lieBracketWithin_add_right

added theorem VectorField.lieBracketWithin_congr'

added theorem VectorField.lieBracketWithin_congr

added theorem VectorField.lieBracketWithin_congr_set'

added theorem VectorField.lieBracketWithin_congr_set

added theorem VectorField.lieBracketWithin_eq

added theorem VectorField.lieBracketWithin_eq_lieBracket

added theorem VectorField.lieBracketWithin_eq_zero_of_eq_zero

added theorem VectorField.lieBracketWithin_eventually_congr_set'

added theorem VectorField.lieBracketWithin_eventually_congr_set

added theorem VectorField.lieBracketWithin_inter

added theorem VectorField.lieBracketWithin_of_isOpen

added theorem VectorField.lieBracketWithin_of_mem_nhds

added theorem VectorField.lieBracketWithin_of_mem_nhdsWithin

added theorem VectorField.lieBracketWithin_self

added theorem VectorField.lieBracketWithin_smul_left

added theorem VectorField.lieBracketWithin_smul_right

added theorem VectorField.lieBracketWithin_subset

added theorem VectorField.lieBracketWithin_swap

added theorem VectorField.lieBracketWithin_univ

added theorem VectorField.lieBracket_add_left

added theorem VectorField.lieBracket_add_right

added theorem VectorField.lieBracket_eq

added theorem VectorField.lieBracket_eq_zero_of_eq_zero

added theorem VectorField.lieBracket_self

added theorem VectorField.lieBracket_smul_left

added theorem VectorField.lieBracket_smul_right

added theorem VectorField.lieBracket_swap