English
Equiv.piCongrLeft acts as a homeomorphism between the indexed product (over i) of Y(e i) and the product over the target index set.
Русский
Equiv.piCongrLeft действует как гомеоморфизм между произведениями по индексу (по i) Y(e i) и произведением по целому множеству индексов.
LaTeX
$$$ (\forall i, Y (e i)) \cong_{\mathrm{Top}} \forall j, Y j, \text{ for a bijection } e: \iota \to \iota'. $$$$
Lean4
/-- 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`.
-/
@[simps! -fullyApplied]
def piUnique {α : Type*} [Unique α] (f : α → Type*) [∀ x, TopologicalSpace (f x)] : (Π t, f t) ≃ₜ f default :=
(Equiv.piUnique f).toHomeomorphOfContinuousOpen (continuous_apply default) (isOpenMap_eval _)
