mathlib documentation

data.nat.pairing

def nat.mkpair  :

Pairing function for the natural numbers.

Equations
def nat.unpair  :

Unpairing function for the natural numbers.

Equations
@[simp]
theorem nat.mkpair_unpair (n : ) :

theorem nat.mkpair_unpair' {n a b : } :
n.unpair = (a, b)a.mkpair b = n

@[simp]
theorem nat.unpair_mkpair (a b : ) :
(a.mkpair b).unpair = (a, b)

theorem nat.unpair_lt {n : } :
1 nn.unpair.fst < n

theorem nat.unpair_le_left (n : ) :

theorem nat.le_mkpair_left (a b : ) :
a a.mkpair b

theorem nat.le_mkpair_right (a b : ) :
b a.mkpair b

theorem nat.unpair_le_right (n : ) :

theorem nat.mkpair_lt_mkpair_left {a₁ a₂ : } (b : ) :
a₁ < a₂a₁.mkpair b < a₂.mkpair b

theorem nat.mkpair_lt_mkpair_right (a : ) {b₁ b₂ : } :
b₁ < b₂a.mkpair b₁ < a.mkpair b₂

theorem set.Union_unpair_prod {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} :
(⋃ (n : ), (s n.unpair.fst).prod (t n.unpair.snd)) = (⋃ (n : ), s n).prod (⋃ (n : ), t n)