English
If g: F →L 𝐆 is a continuous linear map and isUniformInducing, then postcomposing with g yields an isUniformInducing map on the corresponding space of continuous alternating maps.
Русский
Если g: F → L 𝐆 — непрерывное линейное отображение и является IsUniformInducing, то после композиции с g получаем из_uniform-inducing отображение на соответствующее пространство непрерывных чередующих отображений.
LaTeX
$$$$ IsUniformInducing (g.compContinuousAlternatingMap) \\text{ given } IsUniformInducing g $$$$
Lean4
theorem isUniformInducing_postcomp {G : Type*} [AddCommGroup G] [UniformSpace G] [IsUniformAddGroup G] [Module 𝕜 G]
(g : F →L[𝕜] G) (hg : IsUniformInducing g) :
IsUniformInducing (g.compContinuousAlternatingMap : (E [⋀^ι]→L[𝕜] F) → (E [⋀^ι]→L[𝕜] G)) :=
by
rw [← isUniformEmbedding_toContinuousMultilinearMap.1.of_comp_iff]
exact (ContinuousMultilinearMap.isUniformInducing_postcomp g hg).comp isUniformEmbedding_toContinuousMultilinearMap.1
