English
There is a natural homeomorphism between (X ⊕ Y) × Z and (X × Z) ⊕ (Y × Z); i.e., product distributes over sum up to a homeomorphism.
Русский
Существует естественный гомеоморфизм между (X ⊕ Y) × Z и (X × Z) ⊕ (Y × Z); произведение распределяется над суммой до гомеоморфизма.
LaTeX
$$$ (X \\oplus Y) \\times Z \\cong_T (X \\times Z) \\oplus (Y \\times Z) $$$
Lean4
/-- `(X ⊕ Y) × Z` is homeomorphic to `X × Z ⊕ Y × Z`. -/
@[simps!]
def sumProdDistrib : (X ⊕ Y) × Z ≃ₜ (X × Z) ⊕ (Y × Z) :=
Homeomorph.symm <|
(Equiv.sumProdDistrib X Y Z).symm.toHomeomorphOfContinuousOpen
((continuous_inl.prodMap continuous_id).sumElim (continuous_inr.prodMap continuous_id)) <|
(isOpenMap_inl.prodMap IsOpenMap.id).sumElim (isOpenMap_inr.prodMap IsOpenMap.id)
