innerSL_apply_comp_of_isSymmetric

Mathlib.Analysis.InnerProductSpace.Adjoint

URI: https://scilib.ai/kg/mathlib#ContinuousLinearMap.innerSL_apply_comp_of_isSymmetric

English

If f is symmetric, then innerSL x composed with f equals innerSL at f x.

Русский

Если f симметричен, то innerSL x ∘L f = innerSL (f x).

LaTeX

$$innerSL 𝕜 x ∘L f = innerSL 𝕜 (f x) (hf : f.IsSymmetric)$$

Lean4

theorem innerSL_apply_comp_of_isSymmetric (x : E) {f : E →L[𝕜] E} (hf : f.IsSymmetric) :
    innerSL 𝕜 x ∘L f = innerSL 𝕜 (f x) := by ext; simp [hf]

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

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

Разделы

Аффилиация

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