continuous_iff_continuous_uniformFun

English

Let f be defined on α with s ⊆ α compact; a family F(i) with F(i)|_s continuous has Tendsto to f|_s in C(s,β) iff TendstoUniformlyOn F f p on s.

Русский

Пусть f задана на α, s компакт, F(i)|_s непрерывны; тогда Tendsto на ограничениях F к f на s эквивалентно TendstoUniformlyOn на s.

LaTeX

$$$[CompactSpace s] \; (\forall i, ContinuousOn (F(i)) s) \Rightarrow \,\text{Tendsto} (i \mapsto (F(i)|_s)) p (\mathcal{N} f|_s) \iff \text{TendstoUniformlyOn } F f p s$$$

Lean4

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

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