Theorems · Definition · general topology

Homeomorph.piCongr

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

Equiv.piCongr as a homeomorphism: this is the natural homeomorphism Π i₁, Y₁ i ≃ₜ Π i₂, Y₂ i₂ obtained from a bijection ι₁ ≃ ι₂ and homeomorphisms Y₁ i₁ ≃ₜ Y₂ (e i₁) for each i₁ : ι₁.

Defined in

Mathlib.Topology.Homeomorph.Lemmas

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpace