lift_apply

Mathlib.LinearAlgebra.Finsupp.LSum

URI: https://scilib.ai/kg/mathlib#Finsupp.lift_apply

English

The lift map applies to a function f and yields a linear map whose action on x sums f with x.

Русский

Функция lift применяется к данной функции f и порождает линейное отображение, действующее на x через суммирование.

LaTeX

$$$$ llift M R S X f x = lift M R X f x $$$$

Lean4

@[simp]
theorem lift_apply (f) (g) : ((lift M R X) f) g = g.sum fun x r => r • f x :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru