Theorems · Theorem · order theory

Set.singleton_prod_singleton

∀ {α : Type u_1} {β : Type u_2} {a : α} {b : β}, {a} ×ˢ {b} = {(a, b)}

Defined in

Mathlib.Data.Set.Prod

Cited by

9 results in Mathlib

Foundations

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