English
If g is a uniform-inducing map, then post-composing with ContinuousMultilinearMap preserves uniform-inducing property under suitable conditions.
Русский
Если g — равномерно-индуктивное отображение, то после композиции с ContinuousMultilinearMap сохраняется свойство равномерной индукции при подходящих условиях.
LaTeX
$$isUniformInducing_postcomp {G : Type*} [AddCommGroup G] [UniformSpace G] [IsUniformAddGroup G] [Module 𝕜 G] (g : F →L[𝕜] G) (hg : IsUniformInducing g) : IsUniformInducing (g.compContinuousMultilinearMap : ContinuousMultilinearMap 𝕜 E F → ContinuousMultilinearMap 𝕜 E G)$$
Lean4
theorem isUniformInducing_postcomp {G : Type*} [AddCommGroup G] [UniformSpace G] [IsUniformAddGroup G] [Module 𝕜 G]
(g : F →L[𝕜] G) (hg : IsUniformInducing g) :
IsUniformInducing
(g.compContinuousMultilinearMap : ContinuousMultilinearMap 𝕜 E F → ContinuousMultilinearMap 𝕜 E G) :=
by
rw [← isUniformInducing_toUniformOnFun.of_comp_iff]
exact (UniformOnFun.postcomp_isUniformInducing hg).comp isUniformInducing_toUniformOnFun
