Theorems · Definition · general topology

UniformOnFun.uniformEquivPiComm

{α : Type u_1} →
  {ι : Type u_4} →
    (𝔖 : Set (Set α)) →
      (δ : ι → Type u_5) →
        [inst : (i : ι) → UniformSpace (δ i)] → UniformOnFun α ((i : ι) → δ i) 𝔖 ≃ᵤ ((i : ι) → UniformOnFun α (δ i) 𝔖)

The natural bijection between α → Π i, δ i and Π i, α → δ i, upgraded to a uniform isomorphism between α →ᵤ[𝔖] (Π i, δ i) and Π i, α →ᵤ[𝔖] δ i.

Defined in

Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Cited by

0 results in Mathlib

Foundations

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

Assumes

UniformSpace