continuous_iff_continuous_uniformOnFun

English

A map f: X → C(α,β) is continuous iff the corresponding map into UniformOnFun is continuous.

Русский

Отображение f: X → C(α,β) непрерывно тогда и только тогда, когда соответствующее отображение в UniformOnFun непрерывно.

LaTeX

$$$$ Continuous f \\iff Continuous (\\lambda x, ofFun \\{K|IsCompact K\\} (f x)). $$$$

Lean4

/-- `f : X → C(α, β)` is continuous if any only if it is continuous when reinterpreted as a
map `f : X → α →ᵤ[{K | IsCompact K}] β`. -/
theorem continuous_iff_continuous_uniformOnFun {X : Type*} [TopologicalSpace X] (f : X → C(α, β)) :
    Continuous f ↔ Continuous (fun x ↦ ofFun {K | IsCompact K} (f x)) :=
  isUniformEmbedding_toUniformOnFunIsCompact.isInducing.continuous_iff

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