English
The product over a disjoint sum S ⊕ T of a family of spaces is homeomorphic to the product of the product over S and the product over T.
Русский
Производение по дизъюнкту S ⊕ T семейства топологических пространств гомеоморфно произведению (произведению) по S и по T.
LaTeX
$$$\forall S,T\ (A : S\oplus T \to Type),\ [\forall st, TopologicalSpace (A\,st)]\\ (\prod_{st: S\oplus T} A\,st) \cong_{\mathrm{Top}} (\prod_{s:S} A (Sum.inl s)) \times (\prod_{t:T} A (Sum.inr t)).$$$$
Lean4
/-- The product over `S ⊕ T` of a family of topological spaces
is homeomorphic to the product of (the product over `S`) and (the product over `T`).
This is `Equiv.sumPiEquivProdPi` as a `Homeomorph`.
-/
def sumPiEquivProdPi (S T : Type*) (A : S ⊕ T → Type*) [∀ st, TopologicalSpace (A st)] :
(Π (st : S ⊕ T), A st) ≃ₜ (Π (s : S), A (.inl s)) × (Π (t : T), A (.inr t))
where
__ := Equiv.sumPiEquivProdPi _
continuous_toFun := .prodMk (by fun_prop) (by fun_prop)
continuous_invFun := continuous_pi <| by rintro (s | t) <;> dsimp <;> fun_prop
