lieBracketWithin_vectorField — Mathlib

English

If V and W are ContDiffOn 𝕜 n on s, with UniqueDiffOn s and m+1 ≤ n, then lieBracketWithin 𝕜 V W s is ContDiffOn 𝕜 m on s.

Русский

Если V и W гладкие на s в рамках ContDiffOn 𝕜 n, причём s имеет уникальное дифференцируемое множество, и m+1 ≤ n, то lieBracketWithin 𝕜 V W s гладко на s в порядке m.

LaTeX

$$$(hV: ContDiffOn 𝕜 n V s) \\land (hW: ContDiffOn 𝕜 n W s) \\land (hs: UniqueDiffOn 𝕜 s) \\land (hmn: m+1 \\le n) \\Rightarrow ContDiffOn 𝕜 m (lieBracketWithin 𝕜 V W s) s$$$

Lean4

theorem _root_.ContDiffOn.lieBracketWithin_vectorField {m n : WithTop ℕ∞} (hV : ContDiffOn 𝕜 n V s)
    (hW : ContDiffOn 𝕜 n W s) (hs : UniqueDiffOn 𝕜 s) (hmn : m + 1 ≤ n) : ContDiffOn 𝕜 m (lieBracketWithin 𝕜 V W s) s :=
  fun x hx ↦ (hV x hx).lieBracketWithin_vectorField (hW x hx) hs hmn hx

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