preReflection_apply

Mathlib.LinearAlgebra.Reflection

URI: https://scilib.ai/kg/mathlib#Module.preReflection_apply

English

For all R, M, x, f, y we have the value of preReflection applied to y equals y minus f(y) times x.

Русский

Для любых R, M, x, f, y значение preReflection применённое к y равно y минус f(y) умноженное на x.

LaTeX

$$$\operatorname{preReflection}(x,f)(y) = y - (f(y)) \cdot x$$$

Lean4

theorem preReflection_apply : preReflection x f y = y - (f y) • x := by simp [preReflection]

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

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

Разделы

Аффилиация

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