lcomp — Mathlib

English

The application of lcomp to an argument equals the action of the composed maps on that argument.

Русский

Применение lcomp к аргументу равно действию составленных отображений на этот аргумент.

LaTeX

$$$$ lcomp\; f\; g\ x = g\ (f\ x) $$$$

Lean4

/-- Composing a given linear map `M → N` with a linear map `N → P` as a linear map from
`Nₗ →ₗ[R] Pₗ` to `M →ₗ[R] Pₗ`. -/
def lcomp (f : M →ₗ[R] M₂) : (M₂ →ₗ[R] N) →ₗ[S] M →ₗ[R] N :=
  lcompₛₗ _ _ _ f

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