English
Monotonicity of the uniform space with respect to set-system inclusion.
Русский
Монотонность пространств равномерной структуры по включению систем множеств.
LaTeX
$$$$ \text{If } \mathfrak{S}_2 \subseteq \mathfrak{S}_1\text{ then } instUniformSpace_{\sigma} F \mathfrak{S}_1 \leq instUniformSpace_{\sigma} F \mathfrak{S}_2. $$$$
Lean4
theorem isUniformInducing_postcomp {G : Type*} [AddCommGroup G] [UniformSpace G] [IsUniformAddGroup G] {𝕜₃ : Type*}
[NormedField 𝕜₃] [Module 𝕜₃ G] {τ : 𝕜₂ →+* 𝕜₃} {ρ : 𝕜₁ →+* 𝕜₃} [RingHomCompTriple σ τ ρ] [UniformSpace F]
[IsUniformAddGroup F] (g : F →SL[τ] G) (hg : IsUniformInducing g) (𝔖 : Set (Set E)) :
IsUniformInducing (α := UniformConvergenceCLM σ F 𝔖) (β := UniformConvergenceCLM ρ G 𝔖) g.comp :=
by
rw [← (isUniformInducing_coeFn _ _ _).of_comp_iff]
exact (UniformOnFun.postcomp_isUniformInducing hg).comp (isUniformInducing_coeFn _ _ _)
