Theorems · Definition · general topology

Homeomorph.piCongrLeft

{ι : Type u_7} →
  {ι' : Type u_8} →
    {Y : ι' → Type u_9} →
      [inst : (j : ι') → TopologicalSpace (Y j)] → (e : ι ≃ ι') → ((i : ι) → Y (e i)) ≃ₜ ((j : ι') → Y j)

Equiv.piCongrLeft as a homeomorphism: this is the natural homeomorphism Π i, Y (e i) ≃ₜ Π j, Y j obtained from a bijection ι ≃ ι'.

Defined in

Mathlib.Topology.Homeomorph.Lemmas

Cited by

8 results in Mathlib

Foundations

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

Assumes

TopologicalSpace