mlieBracketWithin_const_smul_left

English

Variant: if s,t agree near x then the Lie brackets match on s and t at x.

Русский

Вариант: если s,t совпадают около x, скобки совпадают на s и t в x.

LaTeX

$$Theorem mlieBracketWithin_congr' (hV : EqOn V₁ V s) (hW : EqOn W₁ W s) (hx : x ∈ s) : mlieBracketWithin I V₁ W₁ s x = mlieBracketWithin I V W s x$$

Lean4

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 :=
  by
  simp only [mlieBracketWithin_apply]
  rw [← ContinuousLinearMap.map_smul, mpullbackWithin_smul, lieBracketWithin_const_smul_left]
  · exact hV.differentiableWithinAt_mpullbackWithin_vectorField
  · exact uniqueMDiffWithinAt_iff_inter_range.1 hs

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