Theorems · Definition · functional analysis

ContinuousMultilinearMap.prod

{R : Type u} →
  {ι : Type v} →
    {M₁ : ι → Type w₁} →
      {M₂ : Type w₂} →
        {M₃ : Type w₃} →
          [inst : Semiring R] →
            [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] →
              [inst_2 : AddCommMonoid M₂] →
                [inst_3 : AddCommMonoid M₃] →
                  [inst_4 : (i : ι) → Module R (M₁ i)] →
                    [inst_5 : Module R M₂] →
                      [inst_6 : Module R M₃] →
                        [inst_7 : (i : ι) → TopologicalSpace (M₁ i)] →
                          [inst_8 : TopologicalSpace M₂] →
                            [inst_9 : TopologicalSpace M₃] →
                              ContinuousMultilinearMap R M₁ M₂ →
                                ContinuousMultilinearMap R M₁ M₃ → ContinuousMultilinearMap R M₁ (M₂ × M₃)

The Cartesian product of two continuous multilinear maps, as a continuous multilinear map.

Defined in

Mathlib.Topology.Algebra.Module.Multilinear.Basic

Cited by

16 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoidAddCommMonoidAddCommMonoidModuleModuleModuleTopologicalSpaceTopologicalSpaceTopologicalSpace