Theorems · Definition · general topology

ContinuousMap.toUniformOnFunIsCompact

{α : Type u₁} →
  {β : Type u₂} → [inst : TopologicalSpace α] → [inst_1 : UniformSpace β] → C(α, β) → UniformOnFun α β {K | IsCompact K}

Interpret a bundled continuous map as an element of α →ᵤ[{K | IsCompact K}] β. We use this map to induce the UniformSpace structure on C(α, β).

Defined in

Mathlib.Topology.UniformSpace.CompactConvergence

Cited by

8 results in Mathlib

Foundations

Depth 50 from the axioms · uses propext, Quot.sound

Assumes

TopologicalSpaceUniformSpace