uniformContinuous_comp — Mathlib

English

If G is Lipschitz with constant C, then the map f ↦ (a ↦ G(f(a))) is uniformly continuous on the space of bounded continuous maps α →ᵇ β.

Русский

Если G — Lipschitz с константой C, то отображение f ↦ (a ↦ G(f(a))) является равномерно непрерывным на пространстве ограниченно непрерывных отображений α →ᵇ β.

LaTeX

$$$\\text{UniformContinuous}(\\,f \\mapsto \\mathrm{comp}(G,H)\\,)$$$

Lean4

/-- The composition operator (in the target) with a Lipschitz map is uniformly continuous. -/
theorem uniformContinuous_comp {G : β → γ} {C : ℝ≥0} (H : LipschitzWith C G) :
    UniformContinuous (comp G H : (α →ᵇ β) → α →ᵇ γ) :=
  (lipschitz_comp H).uniformContinuous

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