Registry · Theorem I.T27 tau-effective formalized

I.T27 — Distributivity

Product distributes over coproduct: P x (Q v R) = (P x Q) v (P x R). Both left and right distributivity hold. This makes (E_tau, x, v) a distributive category.

Book I Part 15 Ch. 58

Dependency Graph

Depends on (2)

I.D60 I.D62

Depended on by (2)

I.D63 I.R45

Lean Formalization

Module: TauLib.BookI.Topos.WedgeProduct

Symbol: Tau.Topos.product_distributes_over_coproduct