toContinuousLinearMap — Mathlib

English

Combine a family of continuous alternating maps with the same domain and codomains into a map valued in a product space.

Русский

Объединение семейства непрерывных чередующих отображений с одинаковыми областью и кодом в отображение, значение которого лежит в произведении пространств.

LaTeX

$$$ pi : (\\forall i, M [⋀^ι]→L[R] M' i) \\rightarrow M [⋀^ι]→L[R] \\forall i, M' i $$$

Lean4

/-- If `f` is a continuous alternating map, then `f.toContinuousLinearMap m i` is the continuous
linear map obtained by fixing all coordinates but `i` equal to those of `m`, and varying the
`i`-th coordinate. -/
@[simps! apply]
def toContinuousLinearMap [DecidableEq ι] (m : ι → M) (i : ι) : M →L[R] N :=
  f.1.toContinuousLinearMap m i

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