prodₗᵢ — Mathlib

English

Theorem: For any p in the product space, (ContinuousLinearMap.prodMapL ... ) p equals p.1.prodMap p.2.

Русский

Теорема: для любого p в произведением пространстве, (prodMapL ...) p равно p.1.prodMap p.2.

LaTeX

$$$$\\mathrm{prodMapL}(p) = p.1.\\mathrm{prodMap}~p.2.$$$$

Lean4

/-- `ContinuousLinearMap.prod` as a `LinearIsometryEquiv`. -/
noncomputable def prodₗᵢ (R : Type*) [Semiring R] [Module R F] [Module R G] [ContinuousConstSMul R F]
    [ContinuousConstSMul R G] [SMulCommClass 𝕜 R F] [SMulCommClass 𝕜 R G] :
    (E →L[𝕜] F) × (E →L[𝕜] G) ≃ₗᵢ[R] E →L[𝕜] F × G :=
  ⟨prodₗ R, fun ⟨f, g⟩ => opNorm_prod f g⟩

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