mlieBracketWithin_of_mem_nhds — Mathlib

English

If s is a neighborhood of x, then the Lie bracket within s at x equals the global bracket at x.

Русский

Если s является окрестностью x, то скобка внутри s в x равна глобальной скобке в x.

LaTeX

$$$\mathrm{mlieBracketWithin}(I,V,W,s,x) = \mathrm{mlieBracket}(I,V,W,x)$ when $s \ni x$ and $s$ is a neighborhood$$

Lean4

theorem mlieBracketWithin_of_mem_nhds (h : s ∈ 𝓝 x) : mlieBracketWithin I V W s x = mlieBracket I V W x := by
  rw [← mlieBracketWithin_univ, ← univ_inter s, mlieBracketWithin_inter h]

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