mlieBracketWithin_zero_right — Mathlib

English

The Lie bracket of any vector field with the zero vector field vanishes. In particular, [W,0] is the zero vector field.

Русский

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

LaTeX

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

Lean4

/-- We have `[W, 0] = 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_right : mlieBracketWithin I W 0 s = 0 := by rw [mlieBracketWithin_swap]; simp

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