lie_apply — Mathlib

English

Let α be a set and A be a Lie ring. For any two functions f, g from α to A, the Lie bracket on the function space is defined pointwise, i.e. for every a ∈ α, [f,g](a) = [f(a), g(a)].

Русский

Пусть α — множество, A — Lie-алгебра над кольцом. Для любых f, g: α → A Ли-скобка на множестве функций определяется поэлементно: для каждого a ∈ α выполняется ⁅f,g⁆(a) = ⁅f(a), g(a)⁆.

LaTeX

$$$[f,g](a) = [f(a),\; g(a)].$$$

Lean4

@[simp]
theorem lie_apply {α : Type*} (f g : α → A) (a : α) : ⁅f, g⁆ a = ⁅f a, g a⁆ :=
  rfl

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