Bijection between N and N^2

Stream: Is there code for X?

[Pietro Lavino]

I am working to define refinement of partition given two partitions where partitions are function from N to set \alpha. I have found such a bijection in the form of , and trying to prove associated theorems linv and rinv:

import Mathlib.Algebra.Order.Floor
def pairing_function (k : ℕ × ℕ) : ℕ := (k.1 + k.2) * (k.1 + k.2 + 1) / 2 + k.2

def inverse_pairing_function (k : ℕ) : ℕ × ℕ :=
  let w := Nat.floor (Nat.sqrt (8 * k + 1) - 1) / 2
  let t := w * (w + 1) / 2
  (w - (k - t), k - t)

theorem linv : LeftInverse (inverse_pairing_function) pairing_function:= by sorry
theorem rinv: RightInverse (inverse_pairing_function) pairing_function := by sorry

Is there some easy solution to the two theorems I mention, or is there some bijection with relative forward and backward functions and relative theorem about them being inverse of each other?

[Eric Wieser]

docs#Nat.pairEquiv is one such bijection that already exists

[Pietro Lavino]

thanks!

[Eric Wieser]

I didn't check; is it the same bijection?

[Eric Wieser]

Ah, here's how to check

import Mathlib
--- ...
#eval (fun x y : Fin 5 => pairing_function (x, y))
/-
![![0, 2, 5, 9, 14],
  ![1, 4, 8, 13, 19],
  ![3, 7, 12, 18, 25],
  ![6, 11, 17, 24, 32],
  ![10, 16, 23, 31, 40]]
-/

[Eric Wieser]

Your function does seem like it would be quite nice to have somewhere

[Pietro Lavino]

Why do you think it would be any better than what you sent as it already includes the information of them being inverses if each other?

[Eric Wieser]

If all you need is any bijection, then the one I link is fine. It's at least conceivable that you want that specific bijection in some situations though!

[Asei Inoue]

@Pietro Lavino you may want to see this article (Japanese)

https://zenn.dev/leanja/articles/cantor_pairing

[Asei Inoue]

this article is on Cantor pairing function and its inverse!

[Asei Inoue]

Please ignore Japanese comments and just read code example.