Theorems · Definition · general topology

Homeomorph.piCongrRight

{ι : Type u_7} →
  {Y₁ : ι → Type u_8} →
    {Y₂ : ι → Type u_9} →
      [inst : (i : ι) → TopologicalSpace (Y₁ i)] →
        [inst_1 : (i : ι) → TopologicalSpace (Y₂ i)] → ((i : ι) → Y₁ i ≃ₜ Y₂ i) → ((i : ι) → Y₁ i) ≃ₜ ((i : ι) → Y₂ i)

Equiv.piCongrRight as a homeomorphism: this is the natural homeomorphism Π i, Y₁ i ≃ₜ Π j, Y₂ i obtained from homeomorphisms Y₁ i ≃ₜ Y₂ i for each i.

Defined in

Mathlib.Topology.Homeomorph.Lemmas

Cited by

6 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpace