innerSL_apply_comp — Mathlib

English

Applying innerSL to x and composing with f yields the same as applying innerSL to adjoint f acting on x.

Русский

Применение innerSL к x и композиция с f дают то же, что и применение innerSL к f† acting on x.

LaTeX

$$innerSL 𝕜 x ∘L f = innerSL 𝕜 (adjoint f x)$$

Lean4

theorem innerSL_apply_comp (x : F) (f : E →L[𝕜] F) : innerSL 𝕜 x ∘L f = innerSL 𝕜 (adjoint f x) := by ext;
  simp [adjoint_inner_left]

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