Theorems · Definition · order theory

Setoid.prod

{α : Type u_1} → {β : Type u_2} → Setoid α → Setoid β → Setoid (α × β)

Given types α, β, the product of two equivalence relations r on α and s on β: (x₁, x₂), (y₁, y₂) ∈ α × β are related by r.prod s iff x₁ is related to y₁ by r and x₂ is related to y₂ by s.

Defined in

Mathlib.Data.Setoid.Basic

Cited by

7 results in Mathlib

Foundations

Depth 5 from the axioms · uses no axioms