preReflection_apply_self

Mathlib.LinearAlgebra.Reflection

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

English

If f(x) = 2, then preReflection(x,f)(x) equals −x.

Русский

Если f(x) = 2, то preReflection(x,f)(x) = −x.

LaTeX

$$$\text{preReflection}(x,f)(x) = -x$ при $f(x)=2$$$

Lean4

theorem preReflection_apply_self (h : f x = 2) : preReflection x f x = -x := by rw [preReflection_apply, h, two_smul];
  abel

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

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

Разделы

Аффилиация

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