mlieBracket_const_smul_right — Mathlib

English

Let V and W be vector fields on a manifold, differentiable near a point x. For any scalar c, the Lie bracket is linear in the second argument: [V, cW] = c[V, W] at x.

Русский

Пусть V и W — векторные поля на многообразии, дифференцируемые возле точки x. Для любого скаляра c скобка Ли по второму аргументу линейна: [V, cW] = c[V, W] в точке x.

LaTeX

$$$[V, cW](x) = c\,[V, W](x)$$$

Lean4

theorem mlieBracket_const_smul_right (hW : MDifferentiableAt I I.tangent (fun x ↦ (W x : TangentBundle I M)) x) :
    mlieBracket I V (c • W) x = c • mlieBracket I V W x :=
  by
  simp only [← mlieBracketWithin_univ] at hW ⊢
  exact mlieBracketWithin_const_smul_right hW (uniqueMDiffWithinAt_univ _)

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