lieBracketWithin_of_mem_nhds — Mathlib

English

If s ∈ 𝓝 x, then lieBracketWithin 𝕜 V W s x = lieBracket 𝕜 V W x.

Русский

Если s принадлежит 𝓝 x, то скобка внутри s в x равна обычной скобке Ли в x.

LaTeX

$$$(h: s \\in 𝓝 x) \\Rightarrow lieBracketWithin 𝕜 V W s x = lieBracket 𝕜 V W x$$$

Lean4

theorem lieBracketWithin_of_mem_nhds (h : s ∈ 𝓝 x) : lieBracketWithin 𝕜 V W s x = lieBracket 𝕜 V W x := by
  rw [← lieBracketWithin_univ, ← univ_inter s, lieBracketWithin_inter h]

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