Theorems · Definition · functional analysis

ContinuousMultilinearMap.compContinuousLinearMap

{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 : (i : ι) → AddCommMonoid (M₁' i)] →
                [inst_3 : AddCommMonoid M₄] →
                  [inst_4 : (i : ι) → Module R (M₁ i)] →
                    [inst_5 : (i : ι) → Module R (M₁' i)] →
                      [inst_6 : Module R M₄] →
                        [inst_7 : (i : ι) → TopologicalSpace (M₁ i)] →
                          [inst_8 : (i : ι) → TopologicalSpace (M₁' i)] →
                            [inst_9 : TopologicalSpace M₄] →
                              ContinuousMultilinearMap R M₁' M₄ →
                                ((i : ι) → M₁ i →L[R] M₁' i) → ContinuousMultilinearMap R M₁ M₄

If g is continuous multilinear and f is a collection of continuous linear maps, then g (f₁ m₁, ..., fₙ mₙ) is again a continuous multilinear map, that we call g.compContinuousLinearMap f.

Defined in

Mathlib.Topology.Algebra.Module.Multilinear.Basic

Cited by

46 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoidAddCommMonoidAddCommMonoidModuleModuleModuleTopologicalSpaceTopologicalSpaceTopologicalSpace