toPMap_apply

Mathlib.LinearAlgebra.LinearPMap

URI: https://scilib.ai/kg/mathlib#LinearMap.toPMap_apply

English

The map f.supSpanSingleton x y hx evaluated at the original vector x equals y when domain is extended by x with zero coefficient.

Русский

Отображение f.supSpanSingleton x y hx, применяемое к x, возвращает y при расширении области на x.

LaTeX

$$$$ (f^{\\mathrm{supSpanSingleton}})(x) = y. $$$$

Lean4

@[simp]
theorem toPMap_apply (f : E →ₗ[R] F) (p : Submodule R E) (x : p) : f.toPMap p x = f x :=
  rfl

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

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

Разделы

Аффилиация

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