compContinuousLinearMap — Mathlib

English

If ι is empty, the constant map is alternating; this yields a simple AltMap to N from M with constant value.

Русский

Если ι пуст, константное отображение чередующее; получается простое AltMap в N из M с константным значением.

LaTeX

$$$ constOfIsEmpty R M ι m : M [⋀^ι]→L[R] N $$$

Lean4

/-- If `g` is continuous alternating and `f` is a continuous linear map, then `g (f m₁, ..., f mₙ)`
is again a continuous alternating map, that we call `g.compContinuousLinearMap f`. -/
def compContinuousLinearMap (g : M [⋀^ι]→L[R] N) (f : M' →L[R] M) : M' [⋀^ι]→L[R] N :=
  { g.toAlternatingMap.compLinearMap (f : M' →ₗ[R] M) with
    toContinuousMultilinearMap := g.1.compContinuousLinearMap fun _ => f }

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