prod — Mathlib

English

The Cartesian product of two bounded linear maps is itself a bounded linear map to the product space.

Русский

Дельтаобразная (декартова) сумма двух ограниченных линейных отображений образует ограниченное линейное отображение в произведение пространств.

LaTeX

$$$\text{prod}: (M_1 \to_L[R] M_2) \to (M_1 \to_L[R] M_3) \to M_1 \to_L[R] (M_2 \times M_3)$$$

Lean4

/-- The Cartesian product of two bounded linear maps, as a bounded linear map. -/
protected def prod (f₁ : M₁ →L[R] M₂) (f₂ : M₁ →L[R] M₃) : M₁ →L[R] M₂ × M₃ :=
  ⟨(f₁ : M₁ →ₗ[R] M₂).prod f₂, f₁.2.prodMk f₂.2⟩

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