precompL_apply — Mathlib

English

Let E, Eℓ, F, Fℓ, G, Gℓ be normed spaces over 𝕜, and let L: E →L[𝕜] Fℓ →L[𝕜] Gℓ, u: Eℓ →L[𝕜] E, f ∈ Fℓ, g ∈ Eℓ. Then the precomposition operation satisfies the basic evaluation rule: precompL Eℓ L u f g = L (u g) f.

Русский

Пусть E, Eℓ, F, Fℓ, G, Gℓ — нормированные пространства над 𝕜, а также L: E →L[𝕜] Fℓ →L[𝕜] Gℓ, u: Eℓ →L[𝕜] E, f ∈ Fℓ, g ∈ Eℓ. Тогда выполняется равенство: precompL Eℓ L u f g = L (u g) f.

LaTeX

$$$\operatorname{precompL}_{E_\ell} L\,u\,f\,g = L\bigl(u(g)\bigr) f$$$

Lean4

@[simp]
theorem precompL_apply (L : E →L[𝕜] Fₗ →L[𝕜] Gₗ) (u : Eₗ →L[𝕜] E) (f : Fₗ) (g : Eₗ) : precompL Eₗ L u f g = L (u g) f :=
  rfl

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