prodSumDistrib — Mathlib

English

There is a natural homeomorphism between X × (Y ⊕ Z) and (X × Y) ⊕ (X × Z); i.e., product distributes over sum from the left.

Русский

Существует естественный гомеоморфизм между X × (Y ⊕ Z) и (X × Y) ⊕ (X × Z); произведение распределяется над суммой слева.

LaTeX

$$$ X \\times (Y \\oplus Z) \\cong_T (X \\times Y) \\oplus (X \\times Z) $$$

Lean4

/-- `X × (Y ⊕ Z)` is homeomorphic to `X × Y ⊕ X × Z`. -/
def prodSumDistrib : X × (Y ⊕ Z) ≃ₜ (X × Y) ⊕ (X × Z) :=
  (prodComm _ _).trans <| sumProdDistrib.trans <| sumCongr (prodComm _ _) (prodComm _ _)

Похожие утверждения