lieBracket_vectorField — Mathlib

English

If V and W are ContDiffAt 𝕜 n at x and m+1 ≤ n, then lieBracket 𝕜 V W at x is ContDiffAt 𝕜 m.

Русский

Если V и W гладкие в точке x (ContDiffAt 𝕜 n) и выполняется m+1 ≤ n, то скобка Ли [V, W] в точке x гладкая (ContDiffAt 𝕜 m).

LaTeX

$$$(hV: ContDiffAt 𝕜 n V x) \\land (hW: ContDiffAt 𝕜 n W x) \\land (hmn: m+1 \\le n) \\Rightarrow ContDiffAt 𝕜 m (lieBracket 𝕜 V W) x$$$

Lean4

theorem _root_.ContDiffAt.lieBracket_vectorField {m n : WithTop ℕ∞} (hV : ContDiffAt 𝕜 n V x) (hW : ContDiffAt 𝕜 n W x)
    (hmn : m + 1 ≤ n) : ContDiffAt 𝕜 m (lieBracket 𝕜 V W) x :=
  by
  rw [← contDiffWithinAt_univ] at hV hW ⊢
  simp_rw [← lieBracketWithin_univ]
  exact hV.lieBracketWithin_vectorField hW uniqueDiffOn_univ hmn (mem_univ _)

Похожие утверждения