Theorems · Definition · general topology

UniformEquiv.piCongrLeft

{ι : Type u_4} →
  {ι' : Type u_5} →
    {β : ι' → Type u_6} →
      [inst : (j : ι') → UniformSpace (β j)] → (e : ι ≃ ι') → ((i : ι) → β (e i)) ≃ᵤ ((j : ι') → β j)

Equiv.piCongrLeft as a uniform isomorphism: this is the natural isomorphism Π i, β (e i) ≃ᵤ Π j, β j obtained from a bijection ι ≃ ι'.

Defined in

Mathlib.Topology.UniformSpace.Equiv

Cited by

6 results in Mathlib

Foundations

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

Assumes

UniformSpace