Topology on continuous alternating maps #
In this file we define UniformSpace and TopologicalSpace structures
on the space of continuous alternating maps between topological vector spaces.
The structures are induced by those on ContinuousMultilinearMaps,
and most of the lemmas follow from the corresponding lemmas about ContinuousMultilinearMaps.
instance
ContinuousAlternatingMap.instTopologicalSpace
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{ι : Type u_4}
[NormedField 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
[TopologicalAddGroup F]
:
TopologicalSpace (E [⋀^ι]→L[𝕜] F)
Equations
- ContinuousAlternatingMap.instTopologicalSpace = TopologicalSpace.induced ContinuousAlternatingMap.toContinuousMultilinearMap inferInstance
theorem
ContinuousAlternatingMap.isClosed_range_toContinuousMultilinearMap
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{ι : Type u_4}
[NormedField 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
[TopologicalAddGroup F]
[ContinuousSMul 𝕜 E]
[T2Space F]
:
instance
ContinuousAlternatingMap.instUniformSpace
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{ι : Type u_4}
[NormedField 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[AddCommGroup F]
[Module 𝕜 F]
[UniformSpace F]
[UniformAddGroup F]
:
UniformSpace (E [⋀^ι]→L[𝕜] F)
Equations
- ContinuousAlternatingMap.instUniformSpace = UniformSpace.comap ContinuousAlternatingMap.toContinuousMultilinearMap inferInstance
theorem
ContinuousAlternatingMap.isUniformEmbedding_toContinuousMultilinearMap
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{ι : Type u_4}
[NormedField 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[AddCommGroup F]
[Module 𝕜 F]
[UniformSpace F]
[UniformAddGroup F]
:
IsUniformEmbedding ContinuousAlternatingMap.toContinuousMultilinearMap
@[deprecated ContinuousAlternatingMap.isUniformEmbedding_toContinuousMultilinearMap]
theorem
ContinuousAlternatingMap.uniformEmbedding_toContinuousMultilinearMap
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{ι : Type u_4}
[NormedField 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[AddCommGroup F]
[Module 𝕜 F]
[UniformSpace F]
[UniformAddGroup F]
:
IsUniformEmbedding ContinuousAlternatingMap.toContinuousMultilinearMap
Alias of ContinuousAlternatingMap.isUniformEmbedding_toContinuousMultilinearMap.
theorem
ContinuousAlternatingMap.uniformContinuous_toContinuousMultilinearMap
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{ι : Type u_4}
[NormedField 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[AddCommGroup F]
[Module 𝕜 F]
[UniformSpace F]
[UniformAddGroup F]
:
UniformContinuous ContinuousAlternatingMap.toContinuousMultilinearMap
theorem
ContinuousAlternatingMap.uniformContinuous_coe_fun
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{ι : Type u_4}
[NormedField 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[AddCommGroup F]
[Module 𝕜 F]
[UniformSpace F]
[UniformAddGroup F]
[ContinuousSMul 𝕜 E]
:
UniformContinuous DFunLike.coe
theorem
ContinuousAlternatingMap.uniformContinuous_eval_const
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{ι : Type u_4}
[NormedField 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[AddCommGroup F]
[Module 𝕜 F]
[UniformSpace F]
[UniformAddGroup F]
[ContinuousSMul 𝕜 E]
(x : ι → E)
:
UniformContinuous fun (f : E [⋀^ι]→L[𝕜] F) => f x
instance
ContinuousAlternatingMap.instUniformAddGroup
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{ι : Type u_4}
[NormedField 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[AddCommGroup F]
[Module 𝕜 F]
[UniformSpace F]
[UniformAddGroup F]
:
UniformAddGroup (E [⋀^ι]→L[𝕜] F)
instance
ContinuousAlternatingMap.instUniformContinuousConstSMul
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{ι : Type u_4}
[NormedField 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[AddCommGroup F]
[Module 𝕜 F]
[UniformSpace F]
[UniformAddGroup F]
{M : Type u_5}
[Monoid M]
[DistribMulAction M F]
[SMulCommClass 𝕜 M F]
[ContinuousConstSMul M F]
:
UniformContinuousConstSMul M (E [⋀^ι]→L[𝕜] F)
theorem
ContinuousAlternatingMap.isUniformInducing_postcomp
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{ι : Type u_4}
[NormedField 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[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.compContinuousAlternatingMap
theorem
ContinuousAlternatingMap.completeSpace
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{ι : Type u_4}
[NormedField 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[AddCommGroup F]
[Module 𝕜 F]
[UniformSpace F]
[UniformAddGroup F]
[ContinuousSMul 𝕜 E]
[ContinuousConstSMul 𝕜 F]
[CompleteSpace F]
(h : Topology.RestrictGenTopology {s : Set (ι → E) | Bornology.IsVonNBounded 𝕜 s})
:
CompleteSpace (E [⋀^ι]→L[𝕜] F)
instance
ContinuousAlternatingMap.instCompleteSpace
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{ι : Type u_4}
[NormedField 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[AddCommGroup F]
[Module 𝕜 F]
[UniformSpace F]
[UniformAddGroup F]
[ContinuousSMul 𝕜 E]
[ContinuousConstSMul 𝕜 F]
[CompleteSpace F]
[TopologicalAddGroup E]
[SequentialSpace (ι → E)]
:
CompleteSpace (E [⋀^ι]→L[𝕜] F)
theorem
ContinuousAlternatingMap.isUniformEmbedding_restrictScalars
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{ι : Type u_4}
[NormedField 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[AddCommGroup F]
[Module 𝕜 F]
[UniformSpace F]
[UniformAddGroup F]
(𝕜' : Type u_5)
[NontriviallyNormedField 𝕜']
[NormedAlgebra 𝕜' 𝕜]
[Module 𝕜' E]
[IsScalarTower 𝕜' 𝕜 E]
[Module 𝕜' F]
[IsScalarTower 𝕜' 𝕜 F]
[ContinuousSMul 𝕜 E]
:
@[deprecated ContinuousAlternatingMap.isUniformEmbedding_restrictScalars]
theorem
ContinuousAlternatingMap.uniformEmbedding_restrictScalars
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{ι : Type u_4}
[NormedField 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[AddCommGroup F]
[Module 𝕜 F]
[UniformSpace F]
[UniformAddGroup F]
(𝕜' : Type u_5)
[NontriviallyNormedField 𝕜']
[NormedAlgebra 𝕜' 𝕜]
[Module 𝕜' E]
[IsScalarTower 𝕜' 𝕜 E]
[Module 𝕜' F]
[IsScalarTower 𝕜' 𝕜 F]
[ContinuousSMul 𝕜 E]
:
Alias of ContinuousAlternatingMap.isUniformEmbedding_restrictScalars.
theorem
ContinuousAlternatingMap.uniformContinuous_restrictScalars
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{ι : Type u_4}
[NormedField 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[AddCommGroup F]
[Module 𝕜 F]
[UniformSpace F]
[UniformAddGroup F]
(𝕜' : Type u_5)
[NontriviallyNormedField 𝕜']
[NormedAlgebra 𝕜' 𝕜]
[Module 𝕜' E]
[IsScalarTower 𝕜' 𝕜 E]
[Module 𝕜' F]
[IsScalarTower 𝕜' 𝕜 F]
[ContinuousSMul 𝕜 E]
:
theorem
ContinuousAlternatingMap.isEmbedding_toContinuousMultilinearMap
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{ι : Type u_4}
[NormedField 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
[TopologicalAddGroup F]
:
Topology.IsEmbedding ContinuousAlternatingMap.toContinuousMultilinearMap
@[deprecated ContinuousAlternatingMap.isEmbedding_toContinuousMultilinearMap]
theorem
ContinuousAlternatingMap.embedding_toContinuousMultilinearMap
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{ι : Type u_4}
[NormedField 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
[TopologicalAddGroup F]
:
Topology.IsEmbedding ContinuousAlternatingMap.toContinuousMultilinearMap
Alias of ContinuousAlternatingMap.isEmbedding_toContinuousMultilinearMap.
instance
ContinuousAlternatingMap.instTopologicalAddGroup
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{ι : Type u_4}
[NormedField 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
[TopologicalAddGroup F]
:
TopologicalAddGroup (E [⋀^ι]→L[𝕜] F)
theorem
ContinuousAlternatingMap.continuous_toContinuousMultilinearMap
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{ι : Type u_4}
[NormedField 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
[TopologicalAddGroup F]
:
Continuous ContinuousAlternatingMap.toContinuousMultilinearMap
instance
ContinuousAlternatingMap.instContinuousConstSMul
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{ι : Type u_4}
[NormedField 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
[TopologicalAddGroup F]
{M : Type u_5}
[Monoid M]
[DistribMulAction M F]
[SMulCommClass 𝕜 M F]
[ContinuousConstSMul M F]
:
ContinuousConstSMul M (E [⋀^ι]→L[𝕜] F)
instance
ContinuousAlternatingMap.instContinuousSMul
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{ι : Type u_4}
[NormedField 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
[TopologicalAddGroup F]
[ContinuousSMul 𝕜 F]
:
ContinuousSMul 𝕜 (E [⋀^ι]→L[𝕜] F)
theorem
ContinuousAlternatingMap.hasBasis_nhds_zero_of_basis
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{ι : Type u_4}
[NormedField 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
[TopologicalAddGroup F]
{ι' : Type u_5}
{p : ι' → Prop}
{b : ι' → Set F}
(h : (nhds 0).HasBasis p b)
:
theorem
ContinuousAlternatingMap.hasBasis_nhds_zero
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{ι : Type u_4}
[NormedField 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
[TopologicalAddGroup F]
:
theorem
ContinuousAlternatingMap.isClosedEmbedding_toContinuousMultilinearMap
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{ι : Type u_4}
[NormedField 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
[TopologicalAddGroup F]
[ContinuousSMul 𝕜 E]
[T2Space F]
:
Topology.IsClosedEmbedding ContinuousAlternatingMap.toContinuousMultilinearMap
@[deprecated ContinuousAlternatingMap.isClosedEmbedding_toContinuousMultilinearMap]
theorem
ContinuousAlternatingMap.closedEmbedding_toContinuousMultilinearMap
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{ι : Type u_4}
[NormedField 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
[TopologicalAddGroup F]
[ContinuousSMul 𝕜 E]
[T2Space F]
:
Topology.IsClosedEmbedding ContinuousAlternatingMap.toContinuousMultilinearMap
Alias of ContinuousAlternatingMap.isClosedEmbedding_toContinuousMultilinearMap.
instance
ContinuousAlternatingMap.instContinuousEvalConst
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{ι : Type u_4}
[NormedField 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
[TopologicalAddGroup F]
[ContinuousSMul 𝕜 E]
:
ContinuousEvalConst (E [⋀^ι]→L[𝕜] F) (ι → E) F
@[deprecated ContinuousEvalConst.continuous_eval_const]
theorem
ContinuousAlternatingMap.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
@[deprecated continuous_coeFun]
theorem
ContinuousAlternatingMap.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
ContinuousAlternatingMap.instT2Space
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{ι : Type u_4}
[NormedField 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
[TopologicalAddGroup F]
[ContinuousSMul 𝕜 E]
[T2Space F]
:
instance
ContinuousAlternatingMap.instT3Space
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{ι : Type u_4}
[NormedField 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
[TopologicalAddGroup F]
[ContinuousSMul 𝕜 E]
[T2Space F]
:
theorem
ContinuousAlternatingMap.isEmbedding_restrictScalars
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{ι : Type u_4}
[NormedField 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
[TopologicalAddGroup F]
[ContinuousSMul 𝕜 E]
{𝕜' : Type u_5}
[NontriviallyNormedField 𝕜']
[NormedAlgebra 𝕜' 𝕜]
[Module 𝕜' E]
[IsScalarTower 𝕜' 𝕜 E]
[Module 𝕜' F]
[IsScalarTower 𝕜' 𝕜 F]
:
@[deprecated ContinuousAlternatingMap.isEmbedding_restrictScalars]
theorem
ContinuousAlternatingMap.embedding_restrictScalars
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{ι : Type u_4}
[NormedField 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
[TopologicalAddGroup F]
[ContinuousSMul 𝕜 E]
{𝕜' : Type u_5}
[NontriviallyNormedField 𝕜']
[NormedAlgebra 𝕜' 𝕜]
[Module 𝕜' E]
[IsScalarTower 𝕜' 𝕜 E]
[Module 𝕜' F]
[IsScalarTower 𝕜' 𝕜 F]
:
Alias of ContinuousAlternatingMap.isEmbedding_restrictScalars.
theorem
ContinuousAlternatingMap.continuous_restrictScalars
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{ι : Type u_4}
[NormedField 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
[TopologicalAddGroup F]
[ContinuousSMul 𝕜 E]
{𝕜' : Type u_5}
[NontriviallyNormedField 𝕜']
[NormedAlgebra 𝕜' 𝕜]
[Module 𝕜' E]
[IsScalarTower 𝕜' 𝕜 E]
[Module 𝕜' F]
[IsScalarTower 𝕜' 𝕜 F]
:
def
ContinuousAlternatingMap.restrictScalarsCLM
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{ι : Type u_4}
[NormedField 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
[TopologicalAddGroup F]
[ContinuousSMul 𝕜 E]
(𝕜' : Type u_5)
[NontriviallyNormedField 𝕜']
[NormedAlgebra 𝕜' 𝕜]
[Module 𝕜' E]
[IsScalarTower 𝕜' 𝕜 E]
[Module 𝕜' F]
[IsScalarTower 𝕜' 𝕜 F]
[ContinuousConstSMul 𝕜' F]
:
ContinuousMultilinearMap.restrictScalars as a ContinuousLinearMap.
Equations
- ContinuousAlternatingMap.restrictScalarsCLM 𝕜' = { toFun := ContinuousAlternatingMap.restrictScalars 𝕜', map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
Instances For
@[simp]
theorem
ContinuousAlternatingMap.restrictScalarsCLM_apply
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{ι : Type u_4}
[NormedField 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
[TopologicalAddGroup F]
[ContinuousSMul 𝕜 E]
(𝕜' : Type u_5)
[NontriviallyNormedField 𝕜']
[NormedAlgebra 𝕜' 𝕜]
[Module 𝕜' E]
[IsScalarTower 𝕜' 𝕜 E]
[Module 𝕜' F]
[IsScalarTower 𝕜' 𝕜 F]
[ContinuousConstSMul 𝕜' F]
:
def
ContinuousAlternatingMap.apply
(𝕜 : Type u_1)
(E : Type u_2)
(F : Type u_3)
{ι : Type u_4}
[NormedField 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
[TopologicalAddGroup F]
[ContinuousSMul 𝕜 E]
[ContinuousConstSMul 𝕜 F]
(m : ι → E)
:
The application of a multilinear map as a ContinuousLinearMap.
Equations
- ContinuousAlternatingMap.apply 𝕜 E F m = { toFun := fun (c : E [⋀^ι]→L[𝕜] F) => c m, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
Instances For
@[simp]
theorem
ContinuousAlternatingMap.apply_apply
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{ι : Type u_4}
[NormedField 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
[TopologicalAddGroup F]
[ContinuousSMul 𝕜 E]
[ContinuousConstSMul 𝕜 F]
{m : ι → E}
{c : E [⋀^ι]→L[𝕜] F}
:
(ContinuousAlternatingMap.apply 𝕜 E F m) c = c m
theorem
ContinuousAlternatingMap.hasSum_eval
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{ι : Type u_4}
[NormedField 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
[TopologicalAddGroup F]
[ContinuousSMul 𝕜 E]
{α : Type u_5}
{p : α → E [⋀^ι]→L[𝕜] F}
{q : E [⋀^ι]→L[𝕜] F}
(h : HasSum p q)
(m : ι → E)
:
HasSum (fun (a : α) => (p a) m) (q m)
theorem
ContinuousAlternatingMap.tsum_eval
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{ι : Type u_4}
[NormedField 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
[TopologicalAddGroup F]
[ContinuousSMul 𝕜 E]
[T2Space F]
{α : Type u_5}
{p : α → E [⋀^ι]→L[𝕜] F}
(hp : Summable p)
(m : ι → E)
:
(∑' (a : α), p a) m = ∑' (a : α), (p a) m