mlieBracketWithin_zero_left — Mathlib

English

The Lie bracket of the zero vector field with any vector field vanishes. In other words, for any region s, the bracket [0, W] restricted to s is identically zero.

Русский

Скобка Ли нулевого поля с любым векторным полем равна нулю на любой области.

LaTeX

$$$\,\mathrm{mlieBracketWithin}(I,0,W,s) = 0$$$

Lean4

/-- We have `[0, W] = 0` for all vector fields `W`: this depends on the junk value 0
if `W` is not differentiable. Version within a set. -/
@[simp]
theorem mlieBracketWithin_zero_left : mlieBracketWithin I 0 W s = 0 :=
  by
  ext x
  simp [mlieBracketWithin]

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