isUniformInducing_comp — Mathlib

English

If g is a uniform inducing map, then the postcomposition by g yields an IsUniformInducing map on C-spaces: f ↦ g ∘ f.

Русский

Если g является отображением, индуцирующим униформность, то композиция после g на пространствах функций сохраняет свойство IsUniformInducing.

LaTeX

$$$hg : IsUniformInducing g \Rightarrow IsUniformInducing (\,f\mapsto g\circ f\,)$$$

Lean4

theorem isUniformInducing_comp (g : C(β, δ)) (hg : IsUniformInducing g) :
    IsUniformInducing (ContinuousMap.comp g : C(α, β) → C(α, δ)) :=
  isUniformEmbedding_toUniformOnFunIsCompact.isUniformInducing.of_comp_iff.mp <|
    UniformOnFun.postcomp_isUniformInducing hg |>.comp isUniformEmbedding_toUniformOnFunIsCompact.isUniformInducing

Похожие утверждения