comp_apply

Mathlib.LinearAlgebra.QuadraticForm.Basic

URI: https://scilib.ai/kg/mathlib#QuadraticMap.comp_apply

English

The evaluation of a composed map at x equals the evaluation of the inner map at x under the linear map: (Q.comp f) x = Q (f x).

Русский

Значение композиции в точке x равно значению исходной карты в точке f(x): (Q.comp f) x = Q(f(x)).

LaTeX

$$$ (Q.comp f) x = Q (f x) $ for all x.$$

Lean4

@[simp]
theorem comp_apply (Q : QuadraticMap R N P) (f : M →ₗ[R] N) (x : M) : (Q.comp f) x = Q (f x) :=
  rfl

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

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

Разделы

Аффилиация

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