Theorems · Definition · functional analysis

ContinuousMultilinearMap.domDomCongr

{R : Type u} →
  {ι : Type v} →
    {M₂ : Type w₂} →
      {M₃ : Type w₃} →
        [inst : Semiring R] →
          [inst_1 : AddCommMonoid M₂] →
            [inst_2 : AddCommMonoid M₃] →
              [inst_3 : Module R M₂] →
                [inst_4 : Module R M₃] →
                  [inst_5 : TopologicalSpace M₂] →
                    [inst_6 : TopologicalSpace M₃] →
                      {ι' : Type u_1} →
                        ι ≃ ι' →
                          ContinuousMultilinearMap R (fun x => M₂) M₃ → ContinuousMultilinearMap R (fun x => M₂) M₃

An equivalence of the index set defines an equivalence between the spaces of continuous multilinear maps. This is the forward map of this equivalence.

Defined in

Mathlib.Topology.Algebra.Module.Multilinear.Basic

Cited by

16 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoidAddCommMonoidModuleModuleTopologicalSpaceTopologicalSpace