lieBracketWithin_univ — Mathlib

English

Same additivity in the first argument as above, with a direct equality.

Русский

Та же линейность по первому аргументу: их сумма даёт сумму скобок.

LaTeX

$$$\operatorname{lieBracket}(V+V_1, W)(x) = \operatorname{lieBracket}(V, W)(x) + \operatorname{lieBracket}(V_1, W)(x)$$$

Lean4

@[simp]
theorem lieBracketWithin_univ : lieBracketWithin 𝕜 V W univ = lieBracket 𝕜 V W :=
  by
  ext1 x
  simp [lieBracketWithin, lieBracket]

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