uniformContinuous_comp_left — Mathlib

English

The map f ↦ f ∘ g is uniformly continuous from C(α, γ) to C(α, β) when g ∈ C(α, γ).

Русский

Отображение f ↦ f ∘ g равномерно непрерывно из C(α, γ) в C(α, β), при условии, что g непрерывно на α.

LaTeX

$$$g : C(α, γ) \Rightarrow \text{UniformContinuous}(f \mapsto f \circ g) : C(γ, β) → C(α, β)$$$

Lean4

theorem uniformContinuous_comp_left (g : C(α, γ)) : UniformContinuous (fun f ↦ f.comp g : C(γ, β) → C(α, β)) :=
  isUniformEmbedding_toUniformOnFunIsCompact.uniformContinuous_iff.mpr <|
    UniformOnFun.precomp_uniformContinuous (fun _ hK ↦ hK.image g.continuous) |>.comp
      isUniformEmbedding_toUniformOnFunIsCompact.uniformContinuous

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