Theorems · Theorem · general topology

UniformEquiv.piCongrLeft_toEquiv

∀ {ι : Type u_4} {ι' : Type u_5} {β : ι' → Type u_6} [inst : (j : ι') → UniformSpace (β j)] (e : ι ≃ ι'),
  (UniformEquiv.piCongrLeft e).toEquiv = Equiv.piCongrLeft β e

Defined in

Mathlib.Topology.UniformSpace.Equiv

Cited by

0 results in Mathlib

Foundations

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

Assumes

UniformSpace