Theorems · Definition · functional analysis

ContinuousLinearMap.prodMapL

(𝕜 : Type u_1) →
  [inst : NontriviallyNormedField 𝕜] →
    (M₁ : Type u_5) →
      (M₂ : Type u_6) →
        (M₃ : Type u_7) →
          (M₄ : Type u_8) →
            [inst_1 : SeminormedAddCommGroup M₁] →
              [inst_2 : NormedSpace 𝕜 M₁] →
                [inst_3 : SeminormedAddCommGroup M₂] →
                  [inst_4 : NormedSpace 𝕜 M₂] →
                    [inst_5 : SeminormedAddCommGroup M₃] →
                      [inst_6 : NormedSpace 𝕜 M₃] →
                        [inst_7 : SeminormedAddCommGroup M₄] →
                          [inst_8 : NormedSpace 𝕜 M₄] → (M₁ →L[𝕜] M₂) × (M₃ →L[𝕜] M₄) →L[𝕜] M₁ × M₃ →L[𝕜] M₂ × M₄

ContinuousLinearMap.prodMap as a continuous linear map.

Defined in

Mathlib.Analysis.Normed.Operator.Prod

Cited by

7 results in Mathlib

Foundations

Depth 179 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldSeminormedAddCommGroupNormedSpaceSeminormedAddCommGroupNormedSpaceSeminormedAddCommGroupNormedSpaceSeminormedAddCommGroupNormedSpace