English
If V₁ coincides with V on t and W₁ coincides with W on t, with x in t and t ⊆ s satisfying differentiability, then lieBracketWithin 𝕜 V₁ W₁ t x = lieBracketWithin 𝕜 V W s x.
Русский
Если V₁ совпадает с V на t, а W₁ совпадает с W на t, при этом x ∈ t и t ⊆ s, и задана дифференцируемость, то скобка внутри t совпадает со скобкой внутри s.
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) \\land (hxt: UniqueDiffWithinAt 𝕜 t x) \\land (h₁: t ⊆ s) \\Rightarrow lieBracketWithin 𝕜 V₁ W₁ t x = lieBracketWithin 𝕜 V W s x$$$
Lean4
/-- Variant of `lieBracketWithin_congr_set` where one requires the sets to coincide only in
the complement of a point. -/
theorem lieBracketWithin_congr_set' (y : E) (h : s =ᶠ[𝓝[{ y }ᶜ] x] t) :
lieBracketWithin 𝕜 V W s x = lieBracketWithin 𝕜 V W t x := by simp [lieBracketWithin, fderivWithin_congr_set' _ h]
