prodMap — Mathlib

English

If f1: M1 →L[R] M2 and f2: M3 →L[R] M4 are continuous linear maps, then there is a canonical product map prodMap(f1,f2): M1×M3 →L[R] M2×M4 given by (x,y) ↦ (f1 x, f2 y).

Русский

Если существуют непрерывно линейные отображения f1: M1 →L[R] M2 и f2: M3 →L[R] M4, то существует каноническое отображение-произведение prodMap(f1,f2): M1×M3 →L[R] M2×M4, задающееся (x,y) ↦ (f1 x, f2 y).

LaTeX

$$$\text{prodMap}(f_1,f_2) = (f_1\circ \mathrm{fst},\; f_2\circ \mathrm{snd})$.$$

Lean4

/-- `Prod.map` of two continuous linear maps. -/
def prodMap (f₁ : M₁ →L[R] M₂) (f₂ : M₃ →L[R] M₄) : M₁ × M₃ →L[R] M₂ × M₄ :=
  (f₁.comp (fst R M₁ M₃)).prod (f₂.comp (snd R M₁ M₃))

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