lieBracketWithin_eq_lieBracket — Mathlib

English

If UniqueDiffOn 𝕜 s x and V, W are differentiable at x, then lieBracketWithin 𝕜 V W s x = lieBracket 𝕜 V W x.

Русский

Если s имеет уникальные дифференциалы в x и V, W дифференцируемы в x, то локальная скобка внутри s равна глобальной скобке.

LaTeX

$$$(hs: UniqueDiffWithinAt 𝕜 s x) \\land (hV: DifferentiableAt 𝕜 V x) \\land (hW: DifferentiableAt 𝕜 W x) \\Rightarrow lieBracketWithin 𝕜 V W s x = lieBracket 𝕜 V W x$$$

Lean4

theorem lieBracketWithin_eq_lieBracket (hs : UniqueDiffWithinAt 𝕜 s x) (hV : DifferentiableAt 𝕜 V x)
    (hW : DifferentiableAt 𝕜 W x) : lieBracketWithin 𝕜 V W s x = lieBracket 𝕜 V W x := by
  simp [lieBracketWithin, lieBracket, fderivWithin_eq_fderiv, hs, hV, hW]

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