lieBracketWithin_of_isOpen — Mathlib

English

If s is open and x ∈ s, then lieBracketWithin 𝕜 V W s x = lieBracket 𝕜 V W x.

Русский

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

LaTeX

$$$\\text{IsOpen}(s) \\land x \\in s \\Rightarrow lieBracketWithin 𝕜 V W s x = lieBracket 𝕜 V W x$$$

Lean4

theorem lieBracketWithin_of_isOpen (hs : IsOpen s) (hx : x ∈ s) : lieBracketWithin 𝕜 V W s x = lieBracket 𝕜 V W x :=
  lieBracketWithin_of_mem_nhds (hs.mem_nhds hx)

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