English
There is a homeomorphism between the full product (over ι) of Y j and a split product Y i × (product over j ≠ i).
Русский
Существует гомеоморфизм между полным произведением по ι и разбитым произведением Y_i × (произведение по j ≠ i).
LaTeX
$$$ (\forall j, Y j) \cong_{Top} Y i \times \forall j : { j \ne i }, Y j. $$$
Lean4
/-- A product of topological spaces can be split as the binary product of one of the spaces and
the product of all the remaining spaces. -/
@[simps!]
def piSplitAt (Y : ι → Type*) [∀ j, TopologicalSpace (Y j)] : (∀ j, Y j) ≃ₜ Y i × ∀ j : { j // j ≠ i }, Y j
where
toEquiv := Equiv.piSplitAt i Y
continuous_toFun := (continuous_apply i).prodMk (continuous_pi fun j => continuous_apply j.1)
continuous_invFun :=
continuous_pi fun j => by
dsimp only [Equiv.piSplitAt]
split_ifs with h
· subst h
exact continuous_fst
· exact (continuous_apply _).comp continuous_snd
