English
The forward map UniformOnFun α β 𝔖 → UniformOnFun α β (prod) is uniformly continuous; the inverse map is uniformly continuous as well under the stated assumptions.
Русский
Прямое и обратное отображения между различными вариациями UniformOnFun являются равномерно непрерывными при указанных предпосылках.
LaTeX
$$$\ UniformOnFun.uniformContinuous_ofFun_toFun \;: \ldots$ uniformly continuous.$$
Lean4
/-- The uniformity on `α →ᵤ[𝔖] β` is the same as the uniformity on `α →ᵤ β`,
provided that `Set.univ ∈ 𝔖`.
Here we formulate it as a `UniformEquiv`. -/
def uniformEquivUniformFun (h : univ ∈ 𝔖) : (α →ᵤ[𝔖] β) ≃ᵤ (α →ᵤ β)
where
toFun f := UniformFun.ofFun <| toFun _ f
invFun f := ofFun _ <| UniformFun.toFun f
uniformContinuous_toFun :=
by
simp only [UniformContinuous, (UniformFun.hasBasis_uniformity _ _).tendsto_right_iff]
intro U hU
filter_upwards [UniformOnFun.gen_mem_uniformity _ _ h hU] with f hf x using hf x (mem_univ _)
uniformContinuous_invFun := uniformContinuous_ofUniformFun _ _
