coprod_comp_inl — Mathlib

English

There is a linear equivalence between the product of two maps and the map into a product, extending the usual product structure to the category of continuous linear maps.

Русский

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

LaTeX

$$$$ \text{coprodEquiv} : ((M_1 \to_L[R] M) \times (M_2 \to_L[R] M)) \simeq_L (M_1 \times M_2) \to_L[R] M $$$$

Lean4

@[simp]
theorem coprod_comp_inl (f₁ : M₁ →L[R] M) (f₂ : M₂ →L[R] M) : (f₁.coprod f₂).comp (.inl _ _ _) = f₁ :=
  coe_injective <| LinearMap.coprod_inl ..

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