Theorems · Definition · general topology

Homeomorph.piUnique

{α : Type u_7} →
  [inst : Unique α] → (f : α → Type u_8) → [inst_1 : (x : α) → TopologicalSpace (f x)] → ((t : α) → f t) ≃ₜ f default

The product Π t : α, f t of a family of topological spaces is homeomorphic to the space f ⬝ when α only contains ⬝. This is Equiv.piUnique as a Homeomorph.

Defined in

Mathlib.Topology.Homeomorph.Lemmas

Cited by

3 results in Mathlib

Foundations

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

Assumes

UniqueTopologicalSpace