English
If V and W are ContDiffWithinAt 𝕜 n on a set s at x, the bracket lieBracketWithin 𝕜 V W s is ContDiffWithinAt of order m at x, provided the set s has unique differentiability at x and m+1 ≤ n, with x ∈ s.
Русский
Если V и W belong к классу ContDiffWithinAt 𝕜 n на множестве s в точке x, то скобка Ли внутри s имеет степень дифференцируемости m в точке x, при условии уникальности дифференцируемости s в x и m+1 ≤ n, x ∈ s.
LaTeX
$$$(hV: ContDiffWithinAt 𝕜 n V s x) \land (hW: ContDiffWithinAt 𝕜 n W s x) \land (hs: UniqueDiffOn 𝕜 s) \land (hmn: m+1 \\le n) \land (hx: x \\in s) \\Rightarrow ContDiffWithinAt 𝕜 m (lieBracketWithin 𝕜 V W s) s x$$$
Lean4
theorem _root_.ContDiffWithinAt.lieBracketWithin_vectorField {m n : WithTop ℕ∞} (hV : ContDiffWithinAt 𝕜 n V s x)
(hW : ContDiffWithinAt 𝕜 n W s x) (hs : UniqueDiffOn 𝕜 s) (hmn : m + 1 ≤ n) (hx : x ∈ s) :
ContDiffWithinAt 𝕜 m (lieBracketWithin 𝕜 V W s) s x :=
by
apply ContDiffWithinAt.sub
· exact ContDiffWithinAt.clm_apply (hW.fderivWithin_right hs hmn hx) (hV.of_le (le_trans le_self_add hmn))
· exact ContDiffWithinAt.clm_apply (hV.fderivWithin_right hs hmn hx) (hW.of_le (le_trans le_self_add hmn))
