Documentation

Mathlib.Topology.Algebra.Module.Multilinear.Topology

Topology on continuous multilinear maps #

In this file we define TopologicalSpace and UniformSpace structures on ContinuousMultilinearMap 𝕜 E F, where E i is a family of vector spaces over 𝕜 with topologies and F is a topological vector space.

def ContinuousMultilinearMap.toUniformOnFun {𝕜 : Type u_1} {ι : Type u_2} {E : ιType u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] (f : ContinuousMultilinearMap 𝕜 E F) :
UniformOnFun ((i : ι) → E i) F {s : Set ((i : ι) → E i) | Bornology.IsVonNBounded 𝕜 s}

An auxiliary definition used to define topology on ContinuousMultilinearMap 𝕜 E F.

Equations
Instances For
    theorem ContinuousMultilinearMap.range_toUniformOnFun {𝕜 : Type u_1} {ι : Type u_2} {E : ιType u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [DecidableEq ι] [TopologicalSpace F] :
    Set.range ContinuousMultilinearMap.toUniformOnFun = {f : UniformOnFun ((i : ι) → E i) F {s : Set ((i : ι) → E i) | Bornology.IsVonNBounded 𝕜 s} | Continuous ((UniformOnFun.toFun {s : Set ((i : ι) → E i) | Bornology.IsVonNBounded 𝕜 s}) f) (∀ (m : (i : ι) → E i) (i : ι) (x y : E i), (UniformOnFun.toFun {s : Set ((i : ι) → E i) | Bornology.IsVonNBounded 𝕜 s}) f (Function.update m i (x + y)) = (UniformOnFun.toFun {s : Set ((i : ι) → E i) | Bornology.IsVonNBounded 𝕜 s}) f (Function.update m i x) + (UniformOnFun.toFun {s : Set ((i : ι) → E i) | Bornology.IsVonNBounded 𝕜 s}) f (Function.update m i y)) ∀ (m : (i : ι) → E i) (i : ι) (c : 𝕜) (x : E i), (UniformOnFun.toFun {s : Set ((i : ι) → E i) | Bornology.IsVonNBounded 𝕜 s}) f (Function.update m i (c x)) = c (UniformOnFun.toFun {s : Set ((i : ι) → E i) | Bornology.IsVonNBounded 𝕜 s}) f (Function.update m i x)}
    @[simp]
    theorem ContinuousMultilinearMap.toUniformOnFun_toFun {𝕜 : Type u_1} {ι : Type u_2} {E : ιType u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] (f : ContinuousMultilinearMap 𝕜 E F) :
    (UniformOnFun.toFun {s : Set ((i : ι) → E i) | Bornology.IsVonNBounded 𝕜 s}) f.toUniformOnFun = f
    instance ContinuousMultilinearMap.instTopologicalSpace {𝕜 : Type u_1} {ι : Type u_2} {E : ιType u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] :
    Equations
    • One or more equations did not get rendered due to their size.
    instance ContinuousMultilinearMap.instUniformSpace {𝕜 : Type u_1} {ι : Type u_2} {E : ιType u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [UniformSpace F] [UniformAddGroup F] :
    Equations
    • One or more equations did not get rendered due to their size.
    theorem ContinuousMultilinearMap.isUniformInducing_toUniformOnFun {𝕜 : Type u_1} {ι : Type u_2} {E : ιType u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [UniformSpace F] [UniformAddGroup F] :
    IsUniformInducing ContinuousMultilinearMap.toUniformOnFun
    theorem ContinuousMultilinearMap.isUniformEmbedding_toUniformOnFun {𝕜 : Type u_1} {ι : Type u_2} {E : ιType u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [UniformSpace F] [UniformAddGroup F] :
    IsUniformEmbedding ContinuousMultilinearMap.toUniformOnFun
    @[deprecated ContinuousMultilinearMap.isUniformEmbedding_toUniformOnFun]
    theorem ContinuousMultilinearMap.uniformEmbedding_toUniformOnFun {𝕜 : Type u_1} {ι : Type u_2} {E : ιType u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [UniformSpace F] [UniformAddGroup F] :
    IsUniformEmbedding ContinuousMultilinearMap.toUniformOnFun

    Alias of ContinuousMultilinearMap.isUniformEmbedding_toUniformOnFun.

    theorem ContinuousMultilinearMap.isEmbedding_toUniformOnFun {𝕜 : Type u_1} {ι : Type u_2} {E : ιType u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [UniformSpace F] [UniformAddGroup F] :
    Topology.IsEmbedding ContinuousMultilinearMap.toUniformOnFun
    @[deprecated ContinuousMultilinearMap.isEmbedding_toUniformOnFun]
    theorem ContinuousMultilinearMap.embedding_toUniformOnFun {𝕜 : Type u_1} {ι : Type u_2} {E : ιType u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [UniformSpace F] [UniformAddGroup F] :
    Topology.IsEmbedding ContinuousMultilinearMap.toUniformOnFun

    Alias of ContinuousMultilinearMap.isEmbedding_toUniformOnFun.

    theorem ContinuousMultilinearMap.uniformContinuous_coe_fun {𝕜 : Type u_1} {ι : Type u_2} {E : ιType u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [UniformSpace F] [UniformAddGroup F] [∀ (i : ι), ContinuousSMul 𝕜 (E i)] :
    UniformContinuous DFunLike.coe
    theorem ContinuousMultilinearMap.uniformContinuous_eval_const {𝕜 : Type u_1} {ι : Type u_2} {E : ιType u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [UniformSpace F] [UniformAddGroup F] [∀ (i : ι), ContinuousSMul 𝕜 (E i)] (x : (i : ι) → E i) :
    instance ContinuousMultilinearMap.instUniformAddGroup {𝕜 : Type u_1} {ι : Type u_2} {E : ιType u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [UniformSpace F] [UniformAddGroup F] :
    Equations
    • =
    instance ContinuousMultilinearMap.instUniformContinuousConstSMul {𝕜 : Type u_1} {ι : Type u_2} {E : ιType u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [UniformSpace F] [UniformAddGroup F] {M : Type u_5} [Monoid M] [DistribMulAction M F] [SMulCommClass 𝕜 M F] [ContinuousConstSMul M F] :
    Equations
    • =
    theorem ContinuousMultilinearMap.isUniformInducing_postcomp {𝕜 : Type u_1} {ι : Type u_2} {E : ιType u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [UniformSpace F] [UniformAddGroup F] {G : Type u_5} [AddCommGroup G] [UniformSpace G] [UniformAddGroup G] [Module 𝕜 G] (g : F →L[𝕜] G) (hg : IsUniformInducing g) :
    IsUniformInducing g.compContinuousMultilinearMap
    theorem ContinuousMultilinearMap.completeSpace {𝕜 : Type u_1} {ι : Type u_2} {E : ιType u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [UniformSpace F] [UniformAddGroup F] [∀ (i : ι), ContinuousSMul 𝕜 (E i)] [ContinuousConstSMul 𝕜 F] [CompleteSpace F] (h : Topology.RestrictGenTopology {s : Set ((i : ι) → E i) | Bornology.IsVonNBounded 𝕜 s}) :
    instance ContinuousMultilinearMap.instCompleteSpace {𝕜 : Type u_1} {ι : Type u_2} {E : ιType u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [UniformSpace F] [UniformAddGroup F] [∀ (i : ι), ContinuousSMul 𝕜 (E i)] [ContinuousConstSMul 𝕜 F] [CompleteSpace F] [∀ (i : ι), TopologicalAddGroup (E i)] [SequentialSpace ((i : ι) → E i)] :
    Equations
    • =
    theorem ContinuousMultilinearMap.isUniformEmbedding_restrictScalars {𝕜 : Type u_1} {ι : Type u_2} {E : ιType u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [UniformSpace F] [UniformAddGroup F] (𝕜' : Type u_5) [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [(i : ι) → Module 𝕜' (E i)] [∀ (i : ι), IsScalarTower 𝕜' 𝕜 (E i)] [Module 𝕜' F] [IsScalarTower 𝕜' 𝕜 F] [∀ (i : ι), ContinuousSMul 𝕜 (E i)] :
    @[deprecated ContinuousMultilinearMap.isUniformEmbedding_restrictScalars]
    theorem ContinuousMultilinearMap.uniformEmbedding_restrictScalars {𝕜 : Type u_1} {ι : Type u_2} {E : ιType u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [UniformSpace F] [UniformAddGroup F] (𝕜' : Type u_5) [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [(i : ι) → Module 𝕜' (E i)] [∀ (i : ι), IsScalarTower 𝕜' 𝕜 (E i)] [Module 𝕜' F] [IsScalarTower 𝕜' 𝕜 F] [∀ (i : ι), ContinuousSMul 𝕜 (E i)] :

    Alias of ContinuousMultilinearMap.isUniformEmbedding_restrictScalars.

    theorem ContinuousMultilinearMap.uniformContinuous_restrictScalars {𝕜 : Type u_1} {ι : Type u_2} {E : ιType u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [UniformSpace F] [UniformAddGroup F] (𝕜' : Type u_5) [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [(i : ι) → Module 𝕜' (E i)] [∀ (i : ι), IsScalarTower 𝕜' 𝕜 (E i)] [Module 𝕜' F] [IsScalarTower 𝕜' 𝕜 F] [∀ (i : ι), ContinuousSMul 𝕜 (E i)] :
    instance ContinuousMultilinearMap.instTopologicalAddGroup {𝕜 : Type u_1} {ι : Type u_2} {E : ιType u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] :
    Equations
    • =
    instance ContinuousMultilinearMap.instContinuousConstSMul {𝕜 : Type u_1} {ι : Type u_2} {E : ιType u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] {M : Type u_5} [Monoid M] [DistribMulAction M F] [SMulCommClass 𝕜 M F] [ContinuousConstSMul M F] :
    Equations
    • =
    instance ContinuousMultilinearMap.instContinuousSMul {𝕜 : Type u_1} {ι : Type u_2} {E : ιType u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousSMul 𝕜 F] :
    Equations
    • =
    theorem ContinuousMultilinearMap.hasBasis_nhds_zero_of_basis {𝕜 : Type u_1} {ι : Type u_2} {E : ιType u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] {ι✝ : Type u_5} {p : ι✝Prop} {b : ι✝Set F} (h : (nhds 0).HasBasis p b) :
    (nhds 0).HasBasis (fun (Si : Set ((i : ι) → E i) × ι✝) => Bornology.IsVonNBounded 𝕜 Si.1 p Si.2) fun (Si : Set ((i : ι) → E i) × ι✝) => {f : ContinuousMultilinearMap 𝕜 E F | Set.MapsTo (⇑f) Si.1 (b Si.2)}
    theorem ContinuousMultilinearMap.hasBasis_nhds_zero {𝕜 : Type u_1} {ι : Type u_2} {E : ιType u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] :
    (nhds 0).HasBasis (fun (SV : Set ((i : ι) → E i) × Set F) => Bornology.IsVonNBounded 𝕜 SV.1 SV.2 nhds 0) fun (SV : Set ((i : ι) → E i) × Set F) => {f : ContinuousMultilinearMap 𝕜 E F | Set.MapsTo (⇑f) SV.1 SV.2}
    instance ContinuousMultilinearMap.instContinuousEvalConstForall {𝕜 : Type u_1} {ι : Type u_2} {E : ιType u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] [∀ (i : ι), ContinuousSMul 𝕜 (E i)] :
    ContinuousEvalConst (ContinuousMultilinearMap 𝕜 E F) ((i : ι) → E i) F
    Equations
    • =
    @[deprecated ContinuousEvalConst.continuous_eval_const]
    theorem ContinuousMultilinearMap.continuous_eval_const {F : Type u_1} {α : outParam (Type u_2)} {X : outParam (Type u_3)} {inst✝ : FunLike F α X} {inst✝¹ : TopologicalSpace F} {inst✝² : TopologicalSpace X} [self : ContinuousEvalConst F α X] (x : α) :
    Continuous fun (f : F) => f x

    Alias of ContinuousEvalConst.continuous_eval_const.

    @[deprecated ContinuousEvalConst.continuous_eval_const]
    theorem ContinuousMultilinearMap.continuous_eval_left {F : Type u_1} {α : outParam (Type u_2)} {X : outParam (Type u_3)} {inst✝ : FunLike F α X} {inst✝¹ : TopologicalSpace F} {inst✝² : TopologicalSpace X} [self : ContinuousEvalConst F α X] (x : α) :
    Continuous fun (f : F) => f x

    Alias of ContinuousEvalConst.continuous_eval_const.

    @[deprecated continuous_coeFun]
    theorem ContinuousMultilinearMap.continuous_coe_fun {F : Type u_1} {α : Type u_2} {X : Type u_3} [FunLike F α X] [TopologicalSpace F] [TopologicalSpace X] [ContinuousEvalConst F α X] :
    Continuous DFunLike.coe

    Alias of continuous_coeFun.

    instance ContinuousMultilinearMap.instT2Space {𝕜 : Type u_1} {ι : Type u_2} {E : ιType u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] [∀ (i : ι), ContinuousSMul 𝕜 (E i)] [T2Space F] :
    Equations
    • =
    instance ContinuousMultilinearMap.instT3Space {𝕜 : Type u_1} {ι : Type u_2} {E : ιType u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] [∀ (i : ι), ContinuousSMul 𝕜 (E i)] [T2Space F] :
    Equations
    • =
    theorem ContinuousMultilinearMap.isEmbedding_restrictScalars {𝕜 : Type u_1} {ι : Type u_2} {E : ιType u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] [∀ (i : ι), ContinuousSMul 𝕜 (E i)] {𝕜' : Type u_5} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [(i : ι) → Module 𝕜' (E i)] [∀ (i : ι), IsScalarTower 𝕜' 𝕜 (E i)] [Module 𝕜' F] [IsScalarTower 𝕜' 𝕜 F] :
    @[deprecated ContinuousMultilinearMap.isEmbedding_restrictScalars]
    theorem ContinuousMultilinearMap.embedding_restrictScalars {𝕜 : Type u_1} {ι : Type u_2} {E : ιType u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] [∀ (i : ι), ContinuousSMul 𝕜 (E i)] {𝕜' : Type u_5} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [(i : ι) → Module 𝕜' (E i)] [∀ (i : ι), IsScalarTower 𝕜' 𝕜 (E i)] [Module 𝕜' F] [IsScalarTower 𝕜' 𝕜 F] :

    Alias of ContinuousMultilinearMap.isEmbedding_restrictScalars.

    theorem ContinuousMultilinearMap.continuous_restrictScalars {𝕜 : Type u_1} {ι : Type u_2} {E : ιType u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] [∀ (i : ι), ContinuousSMul 𝕜 (E i)] {𝕜' : Type u_5} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [(i : ι) → Module 𝕜' (E i)] [∀ (i : ι), IsScalarTower 𝕜' 𝕜 (E i)] [Module 𝕜' F] [IsScalarTower 𝕜' 𝕜 F] :
    def ContinuousMultilinearMap.restrictScalarsLinear {𝕜 : Type u_1} {ι : Type u_2} {E : ιType u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] [∀ (i : ι), ContinuousSMul 𝕜 (E i)] (𝕜' : Type u_5) [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [(i : ι) → Module 𝕜' (E i)] [∀ (i : ι), IsScalarTower 𝕜' 𝕜 (E i)] [Module 𝕜' F] [IsScalarTower 𝕜' 𝕜 F] [ContinuousConstSMul 𝕜' F] :

    ContinuousMultilinearMap.restrictScalars as a ContinuousLinearMap.

    Equations
    Instances For
      @[simp]
      theorem ContinuousMultilinearMap.restrictScalarsLinear_apply {𝕜 : Type u_1} {ι : Type u_2} {E : ιType u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] [∀ (i : ι), ContinuousSMul 𝕜 (E i)] (𝕜' : Type u_5) [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [(i : ι) → Module 𝕜' (E i)] [∀ (i : ι), IsScalarTower 𝕜' 𝕜 (E i)] [Module 𝕜' F] [IsScalarTower 𝕜' 𝕜 F] [ContinuousConstSMul 𝕜' F] :
      def ContinuousMultilinearMap.apply (𝕜 : Type u_1) {ι : Type u_2} (E : ιType u_3) (F : Type u_4) [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] [∀ (i : ι), ContinuousSMul 𝕜 (E i)] [ContinuousConstSMul 𝕜 F] (m : (i : ι) → E i) :

      The application of a multilinear map as a ContinuousLinearMap.

      Equations
      Instances For
        @[simp]
        theorem ContinuousMultilinearMap.apply_apply {𝕜 : Type u_1} {ι : Type u_2} {E : ιType u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] [∀ (i : ι), ContinuousSMul 𝕜 (E i)] [ContinuousConstSMul 𝕜 F] {m : (i : ι) → E i} {c : ContinuousMultilinearMap 𝕜 E F} :
        theorem ContinuousMultilinearMap.hasSum_eval {𝕜 : Type u_1} {ι : Type u_2} {E : ιType u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] [∀ (i : ι), ContinuousSMul 𝕜 (E i)] {α : Type u_5} {p : αContinuousMultilinearMap 𝕜 E F} {q : ContinuousMultilinearMap 𝕜 E F} (h : HasSum p q) (m : (i : ι) → E i) :
        HasSum (fun (a : α) => (p a) m) (q m)
        theorem ContinuousMultilinearMap.tsum_eval {𝕜 : Type u_1} {ι : Type u_2} {E : ιType u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] [∀ (i : ι), ContinuousSMul 𝕜 (E i)] [T2Space F] {α : Type u_5} {p : αContinuousMultilinearMap 𝕜 E F} (hp : Summable p) (m : (i : ι) → E i) :
        (∑' (a : α), p a) m = ∑' (a : α), (p a) m