lieBracket_vectorField — Mathlib

English

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

Русский

Если V и W гладкие на всем пространстве, и m+1 ≤ n, то скобка Ли [V, W] гладкая на уровне m.

LaTeX

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

Lean4

theorem _root_.ContDiff.lieBracket_vectorField {m n : WithTop ℕ∞} (hV : ContDiff 𝕜 n V) (hW : ContDiff 𝕜 n W)
    (hmn : m + 1 ≤ n) : ContDiff 𝕜 m (lieBracket 𝕜 V W) :=
  contDiff_iff_contDiffAt.2 (fun _ ↦ hV.contDiffAt.lieBracket_vectorField hW.contDiffAt hmn)

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