prod_map_equivL — Mathlib

English

The map prodMapL is a continuous map sending a pair of continuous linear maps to their product map.

Русский

Отображение prodMapL непрерывно отправляет пару непрерывных линейных отображений в их произведение отображений.

LaTeX

$$$$\\mathrm{prodMapL} : (M_1 \\to_L M_2) \\times (M_3 \\to_L M_4) \\to_L (M_1 \\to_L (M_2 \\times M_4))$$$$

Lean4

theorem _root_.Continuous.prod_map_equivL {f : X → M₁ ≃L[𝕜] M₂} {g : X → M₃ ≃L[𝕜] M₄}
    (hf : Continuous fun x => (f x : M₁ →L[𝕜] M₂)) (hg : Continuous fun x => (g x : M₃ →L[𝕜] M₄)) :
    Continuous fun x => ((f x).prodCongr (g x) : M₁ × M₃ →L[𝕜] M₂ × M₄) :=
  (prodMapL 𝕜 M₁ M₂ M₃ M₄).continuous.comp (hf.prodMk hg)

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