mlieBracketWithin_univ

Mathlib.Geometry.Manifold.VectorField.LieBracket

URI: https://scilib.ai/kg/mathlib#VectorField.mlieBracketWithin_univ

English

If V and W vanish at a point x, then their Lie bracket within also vanishes at x.

Русский

Если V и W равны нулю в точке x, то их скобка Ли внутри также равна нулю в x.

LaTeX

$$mlieBracketWithin_eq_zero_of_eq_zero (hV : V x = 0) (hW : W x = 0) : mlieBracketWithin I V W s x = 0$$

Lean4

@[simp]
theorem mlieBracketWithin_univ : mlieBracketWithin I V W univ = mlieBracket I V W :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru