English
Let i be a fixed index in ι and Y a topological space. The space of all functions ι → Y is naturally split as the product of the i-th copy Y with the product of all the remaining copies, i.e. (ι → Y) ≅ Y × ({ j | j ≠ i } → Y) via splitting the i-th coordinate.
Русский
Пусть i – фиксированный индекс в ι и Y – топологическое пространство. Пространство всех отображений ι → Y гомеоморфно произведению Y × ({ j | j ≠ i } → Y), полученному разбиением i-й координаты: (ι → Y) ≅ Y × ({ j | j ≠ i } → Y).
LaTeX
$$$$(\iota \to Y) \simeq_{\mathrm{Top}} Y \times ({ j \;\mid\; j \neq i } \to Y).$$$$
Lean4
/-- A product of copies of a topological space can be split as the binary product of one copy and
the product of all the remaining copies. -/
@[simps!]
def funSplitAt : (ι → Y) ≃ₜ Y × ({ j // j ≠ i } → Y) :=
piSplitAt i _
