Commit 2025-02-28 16:22 11100128

View on Github →

feat: the Lie bracket of vector fields on manifolds (#22013)

Estimated changes

Modified Mathlib/Geometry/Manifold/VectorField.lean

added theorem DifferentiableWithinAt.mlieBracketWithin_congr_mono

added theorem Filter.EventuallyEq.mlieBracketWithin_vectorField'

added theorem Filter.EventuallyEq.mlieBracketWithin_vectorField_eq

added theorem Filter.EventuallyEq.mlieBracketWithin_vectorField_eq_nhds

added theorem Filter.EventuallyEq.mlieBracketWithin_vectorField_eq_of_mem

added theorem Filter.EventuallyEq.mlieBracket_vectorField_eq

added theorem MDifferentiableWithinAt.differentiableWithinAt_mpullbackWithin_vectorField

added def VectorField.mlieBracket

added def VectorField.mlieBracketWithin

added theorem VectorField.mlieBracketWithin_add_left

added theorem VectorField.mlieBracketWithin_add_right

added theorem VectorField.mlieBracketWithin_apply

added theorem VectorField.mlieBracketWithin_congr'

added theorem VectorField.mlieBracketWithin_congr

added theorem VectorField.mlieBracketWithin_congr_set'

added theorem VectorField.mlieBracketWithin_congr_set

added theorem VectorField.mlieBracketWithin_def

added theorem VectorField.mlieBracketWithin_eq_lieBracketWithin

added theorem VectorField.mlieBracketWithin_eq_mlieBracket

added theorem VectorField.mlieBracketWithin_eq_zero_of_eq_zero

added theorem VectorField.mlieBracketWithin_eventually_congr_set'

added theorem VectorField.mlieBracketWithin_eventually_congr_set

added theorem VectorField.mlieBracketWithin_inter

added theorem VectorField.mlieBracketWithin_of_isOpen

added theorem VectorField.mlieBracketWithin_of_mem_nhds

added theorem VectorField.mlieBracketWithin_of_mem_nhdsWithin

added theorem VectorField.mlieBracketWithin_self

added theorem VectorField.mlieBracketWithin_smul_left

added theorem VectorField.mlieBracketWithin_smul_right

added theorem VectorField.mlieBracketWithin_subset

added theorem VectorField.mlieBracketWithin_swap

added theorem VectorField.mlieBracketWithin_swap_apply

added theorem VectorField.mlieBracketWithin_univ

added theorem VectorField.mlieBracket_add_left

added theorem VectorField.mlieBracket_add_right

added theorem VectorField.mlieBracket_self

added theorem VectorField.mlieBracket_smul_left

added theorem VectorField.mlieBracket_smul_right

added theorem VectorField.mlieBracket_swap

added theorem VectorField.mlieBracket_swap_apply