Theorems · Theorem · logic and foundations

Equiv.sigmaSumDistrib_symm_apply

∀ {ι : Type u_11} (α : ι → Type u_9) (β : ι → Type u_10) (a : (i : ι) × α i ⊕ (i : ι) × β i),
  (Equiv.sigmaSumDistrib α β).symm a = Sum.elim (Sigma.map id fun x => Sum.inl) (Sigma.map id fun x => Sum.inr) a

Defined in

Mathlib.Logic.Equiv.Sum

Cited by

0 results in Mathlib

Foundations

Depth 14 from the axioms · uses Quot.sound