prod_map_equivL — Mathlib

English

prodMapL is a canonical linear isometry equivalence between the product of two operator spaces and the operator space of the product.

Русский

prodMapL — каноническое линейное изометрическое эквивалентное отображение между произведением двух пространств операторов и пространством операторов в произведении.

LaTeX

$$$$\\mathrm{prodG} : (E \\to_L F) \\times (E \\to_L G) \\cong_i (E \\to_L (F \\times G)).$$$$

Lean4

theorem _root_.ContinuousOn.prod_map_equivL {f : X → M₁ ≃L[𝕜] M₂} {g : X → M₃ ≃L[𝕜] M₄} {s : Set X}
    (hf : ContinuousOn (fun x => (f x : M₁ →L[𝕜] M₂)) s) (hg : ContinuousOn (fun x => (g x : M₃ →L[𝕜] M₄)) s) :
    ContinuousOn (fun x => ((f x).prodCongr (g x) : M₁ × M₃ →L[𝕜] M₂ × M₄)) s :=
  hf.prod_mapL _ hg

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