English
If V is differentiable within s at x, V₁ ≡ V on t, and V₁ x = V x, and similarly for W, with W₁ ≡ W on t and x, then lieBracketWithin 𝕜 V₁ W₁ t x = lieBracketWithin 𝕜 V W s x.
Русский
Если V дифференцируем внутри s в x, V₁ совпадает с V на t, и V₁ x = V x, а для W аналогично, то скобка внутри t совпадает со скобкой внутри s в x.
LaTeX
$$$(hV: DifferentiableWithinAt 𝕜 V s x) \\land (hVs: EqOn V₁ V t) \\land (hVx: V₁ x = V x) \\land (hW: DifferentiableWithinAt 𝕜 W s x) \\land (hWs: EqOn W₁ W t) \\land (hWx: W₁ x = W x) \\Rightarrow lieBracketWithin 𝕜 V₁ W₁ t x = lieBracketWithin 𝕜 V W s x$$$
Lean4
theorem _root_.DifferentiableWithinAt.lieBracketWithin_congr_mono (hV : DifferentiableWithinAt 𝕜 V s x)
(hVs : EqOn V₁ V t) (hVx : V₁ x = V x) (hW : DifferentiableWithinAt 𝕜 W s x) (hWs : EqOn W₁ W t) (hWx : W₁ x = W x)
(hxt : UniqueDiffWithinAt 𝕜 t x) (h₁ : t ⊆ s) : lieBracketWithin 𝕜 V₁ W₁ t x = lieBracketWithin 𝕜 V W s x := by
simp [lieBracketWithin, hV.fderivWithin_congr_mono, hW.fderivWithin_congr_mono, hVs, hVx, hWs, hWx, hxt, h₁]
