mlieBracket_const_smul_left — Mathlib

English

Variant: mlieBracketWithin_congr' with scalar smul and V, W data preserved yields equality with scalar multiple.

Русский

Вариант: при конгруэнции и скалярном умножении сохраняется равенство.

LaTeX

$$Theorem mlieBracketWithin_const_smul_left (hV : MDifferentiableWithinAt I I.tangent (fun x => (V x : TangentBundle I M)) s x) (hs : UniqueMDiffWithinAt I s x) : mlieBracketWithin I (c • V) W s x = c • mlieBracketWithin I V W s x$$

Lean4

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

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