English
If f is a uniform inducing map, then the postcomposition operator (f ∘ ·) on α →ᵤ γ is uniform inducing.
Русский
Если f — равномерно индуцирующее отображение, то пост-композиция (f ∘ ·) на α →ᵤ γ равномерно индуцирует.
LaTeX
$$$$ \text{If } f: γ \to β \text{ is uniform inducing, then } (f \circ \cdot): (α \to^{u} γ) \to (α \to^{u} β) \text{ is uniform inducing}. $$$$
Lean4
/-- Post-composition by a uniform inducing function is
a uniform inducing function for the uniform structures of uniform convergence.
More precisely, if `f : γ → β` is uniform inducing,
then `(f ∘ ·) : (α →ᵤ γ) → (α →ᵤ β)` is uniform inducing. -/
theorem postcomp_isUniformInducing [UniformSpace γ] {f : γ → β} (hf : IsUniformInducing f) :
IsUniformInducing (ofFun ∘ (f ∘ ·) ∘ toFun : (α →ᵤ γ) → α →ᵤ β) :=
⟨((UniformFun.hasBasis_uniformity _ _).comap _).eq_of_same_basis <|
UniformFun.hasBasis_uniformity_of_basis _ _ (hf.basis_uniformity (𝓤 β).basis_sets)⟩
