Theorems · Theorem · general topology

UniformEquiv.piCongrLeft_symm_apply

∀ {ι : Type u_4} {ι' : Type u_5} {X : ι' → Type u_6} [inst : (j : ι') → UniformSpace (X j)] (e : ι ≃ ι'),
  ⇑(UniformEquiv.piCongrLeft e).symm = fun x1 x2 => x1 (e x2)

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