Theorems · Definition · logic and foundations

Set.prod

{α : Type u} → {β : Type v} → Set α → Set β → Set (α × β)

The Cartesian product Set.prod s t is the set of (a, b) such that a ∈ s and b ∈ t.

Defined in

Mathlib.Data.Set.Operations

Cited by

6 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms