uniformContinuous_ofUniformFun — Mathlib

English

The map f ↦ ofFun 𝔖 (UniformFun.toFun f) from UniformOnFun α β 𝔖 to UniformFun α β is uniformly continuous.

Русский

Отображение f ↦ ofFun 𝔖 (UniformFun.toFun f) между пространствами является равномерно непрерывным.

LaTeX

$$$\text{UniformContinuous } (f \mapsto \mathrm{ofFun}\ 𝔖 (\mathrm{UniformFun.toFun}\ f))$.$$

Lean4

theorem uniformContinuous_ofUniformFun : UniformContinuous fun f : α →ᵤ β ↦ ofFun 𝔖 (UniformFun.toFun f) :=
  by
  simp only [UniformContinuous, UniformOnFun.uniformity_eq, tendsto_iInf, tendsto_principal,
    (UniformFun.hasBasis_uniformity _ _).eventually_iff]
  exact fun _ _ U hU ↦ ⟨U, hU, fun f hf x _ ↦ hf x⟩

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