Theorems · Definition · logic and foundations

Equiv.prodUnique

(α : Type u_9) → (β : Type u_10) → [Unique β] → α × β ≃ α

Any Unique type is a right identity for type product up to equivalence.

Defined in

Mathlib.Logic.Equiv.Prod

Cited by

6 results in Mathlib

Foundations

Depth 18 from the axioms · uses propext, Quot.sound

Assumes

Unique