Theorems · Definition · functional analysis

ContinuousMultilinearMap.ofSubsingleton

(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₃] →
                      [Subsingleton ι] → ι → (M₂ →L[R] M₃) ≃ ContinuousMultilinearMap R (fun x => M₂) M₃

The natural equivalence between continuous linear maps from M₂ to M₃ and continuous 1-multilinear maps from M₂ to M₃.

Defined in

Mathlib.Topology.Algebra.Module.Multilinear.Basic

Cited by

13 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoidAddCommMonoidModuleModuleTopologicalSpaceTopologicalSpaceSubsingleton