lieBracketWithin_of_mem_nhdsWithin

English

If t lies in the neighborhood of x within s (st ∈ 𝓝[s] x), then lieBracketWithin 𝕜 V W s x equals lieBracketWithin 𝕜 V W t x.

Русский

Если множество t совпадает внутри окрестности x по отношению к s, то скобка Ли внутри s в точке x равна скобке внутри t.

LaTeX

$$$(st: t \\in 𝓝[s] x) \\Rightarrow lieBracketWithin 𝕜 V W s x = lieBracketWithin 𝕜 V W t x$$$

Lean4

theorem lieBracketWithin_of_mem_nhdsWithin (st : t ∈ 𝓝[s] x) (hs : UniqueDiffWithinAt 𝕜 s x)
    (hV : DifferentiableWithinAt 𝕜 V t x) (hW : DifferentiableWithinAt 𝕜 W t x) :
    lieBracketWithin 𝕜 V W s x = lieBracketWithin 𝕜 V W t x := by
  simp [lieBracketWithin, fderivWithin_of_mem_nhdsWithin st hs hV, fderivWithin_of_mem_nhdsWithin st hs hW]

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