prodEquiv — Mathlib

English

There is a canonical linear equivalence between the product of two continuous linear maps and a single continuous linear map into a product: (M →L M2) × (M →L M3) ≃_lin[M] M →L (M2 × M3).

Русский

Существует каноническое линейное эквивалентное отображение между произведением двух непрерывных линейных отображений и одним отображением в произведение: (M →L M2) × (M →L M3) ≃_lin M →L (M2 × M3).

LaTeX

$$$$ (M \to_L M_2) \times (M \to_L M_3) \simeq_{\text{Lin}} M \to_L (M_2 \times M_3) $$$$

Lean4

/-- `ContinuousLinearMap.prod` as an `Equiv`. -/
@[simps apply]
def prodEquiv : (M →L[R] M₂) × (M →L[R] M₃) ≃ (M →L[R] M₂ × M₃)
    where
  toFun f := f.1.prod f.2
  invFun f := ⟨(fst _ _ _).comp f, (snd _ _ _).comp f⟩

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