Theorems · Definition · logic and foundations

Equiv.Set.prod

{α : Type u_3} → {β : Type u_4} → (s : Set α) → (t : Set β) → ↑(s ×ˢ t) ≃ ↑s × ↑t

The set product of two sets is equivalent to the type product of their coercions to types.

Defined in

Mathlib.Logic.Equiv.Set

Cited by

9 results in Mathlib

Foundations

Depth 11 from the axioms · uses no axioms