bracket_apply — Mathlib

English

The bracket in a direct sum of Lie modules is computed componentwise: the i-th component of [x,y] equals [x_i,y_i].

Русский

Скалярный скобочный оператор в прямой сумме модулей Ли вычисляется по компонентам: (x,y) в i-й компоненте даёт [x_i,y_i].

LaTeX

$$For all x,y in ⨁ i, L_i and i, [x,y]_i = [x_i,y_i].$$

Lean4

@[simp]
theorem bracket_apply (x y : ⨁ i, L i) (i : ι) : ⁅x, y⁆ i = ⁅x i, y i⁆ :=
  zipWith_apply _ _ x y i

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