Embedding an analytic equivalence relation in the transitive closure of a Borel relation

EDWARD J GREEN

This illustrates the concept of [A]_P from the footnote on the first page.

Specifically, if P is the partition of ℕ into even and odd numbers and A is the set of prime numbers, then we show that [A]_P = ℕ.

def f_Green : ℕ → Fin 2

Equations

• f_Green n = ⟨n % 2, ⋯⟩

def p : ℕ → ℕ → Prop

Equations

• p i j = (f_Green i = f_Green j)

def P_Green : Set (Set ℕ)

Equations

• P_Green = {{a : ℕ | f_Green a = 0}, {a : ℕ | f_Green a = 1}}

def A : Set ℕ

Equations

• A i = Nat.Prime i

theorem primes_odd_even (i : Fin 2) : ∃ (n : ℕ), Nat.Prime n ∧ f_Green n = i

theorem A_p (n : ℕ) : ∃ a ∈ A, p n a

theorem π_P (n : ℕ) : ∃ π ∈ P_Green, π ∩ A ≠ ∅