lmk_apply

Mathlib.LinearAlgebra.DFinsupp

URI: https://scilib.ai/kg/mathlib#DFinsupp.lmk_apply

English

For all s and x, (lmk s)(x) = mk s x.

Русский

Для всех s и x выполняется (lmk s)(x) = mk s x.

LaTeX

$$$\\mathrm{lmk}\\,s\\; x = \\mathrm{mk}\\,s\\; x$$$

Lean4

theorem lmk_apply (s : Finset ι) (x) : (lmk s : _ →ₗ[R] Π₀ i, M i) x = mk s x :=
  rfl

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

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

Разделы

Аффилиация

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