mlieBracketWithin_of_isOpen — Mathlib

English

Equality of the Lie bracket within s and within t holds when the same holds on nhds of x.

Русский

Равенство скобки Ли внутри s и внутри t сохраняется, если они совпадают на окрестности точки x.

LaTeX

$$$\mathrm{nhds}(x)\text{-}$EventuallyEq $\mathrm{mlieBracketWithin}(I,V₁,W₁,s) = \mathrm{mlieBracketWithin}(I,V,W,s)$ and similarly for t$$

Lean4

theorem mlieBracketWithin_of_isOpen (hs : IsOpen s) (hx : x ∈ s) : mlieBracketWithin I V W s x = mlieBracket I V W x :=
  mlieBracketWithin_of_mem_nhds (hs.mem_nhds hx)

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