Theorems · Theorem · general topology

ContinuousOn.continuous_domRestrict_iff_continuous_uniformOnFun

∀ {α : Type u₁} {β : Type u₂} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {X : Type u_1}
  [inst_2 : TopologicalSpace X] {f : X → α → β} {s : Set α} (hf : ∀ (x : X), ContinuousOn (f x) s) [CompactSpace ↑s],
  (Continuous fun x => { toFun := s.domRestrict (f x), continuous_toFun := ⋯ }) ↔
    Continuous fun x => (UniformOnFun.ofFun {s}) (f x)

A family f : X → α → β, each of which is continuous on a compact set s : Set α is continuous in the topology X → α →ᵤ[{s}] β if and only if the family of continuous restrictions X → C(s, β) is continuous.

Defined in

Mathlib.Topology.UniformSpace.CompactConvergence

Cited by

1 results in Mathlib

Foundations

Depth 92 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceUniformSpaceTopologicalSpaceCompactSpace