English
Under a locally finite cover by compact precomposition maps φi, the uniform space on C(α,β) is the infimum over i of comaps by φi.
Русский
При локально конечном покрытии отображениями φi равномерная структура пространства C(α,β) является инфимом по всем сопутствующим предкомпозиций φi.
LaTeX
$$$\text{UniformSpace } C(α, β) = \bigwedge_i \text{comap}(\cdot, φ_i)$$$
Lean4
/-- 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. -/
theorem _root_.ContinuousOn.continuous_restrict_iff_continuous_uniformOnFun {X : Type*} [TopologicalSpace X]
{f : X → α → β} {s : Set α} (hf : ∀ x, ContinuousOn (f x) s) [CompactSpace s] :
Continuous (fun x ↦ ⟨_, (hf x).restrict⟩ : X → C(s, β)) ↔ Continuous (fun x ↦ ofFun { s } (f x)) :=
by
rw [ContinuousMap.continuous_iff_continuous_uniformFun, UniformOnFun.continuous_rng_iff]
simp [Function.comp_def]
