PFA and complemented subspaces of ℓ_∞/c₀

Alan Dow

Section 2 of the paper starts: Let A_n, n ∈ ℕ be a partition of ℕ into infinite sets. Here we prove formally that there exists a partition of ℕ into infinitely many infinite sets. The idea is to use the 2-adic valuation. (We first prove it for just two sets as a warmup.)

We also introduce the ideals A⊥ and I (introduced on page 2 of the paper) and prove A⊥ ⊆ I.

def E : Set ℕ

Equations

• E k = Even k

def O : Set ℕ

Equations

• O k = Odd k

theorem infiniteEven : Infinite ↑E

theorem infiniteOdd : Infinite ↑O

theorem disjointEvenOdd : Disjoint E O

theorem exhaustiveEvenOdd : E ∪ O = Set.univ

def A_Dow : ℕ → Set ℕ

Equations

• A_Dow n k = (padicValNat 2 k = n)

theorem exhaustiveA_Dow : ⋃ (n : ℕ), A_Dow n = Set.univ

theorem disjointA_Dow {m : ℕ} {n : ℕ} (h : m ≠ n) : Disjoint (A_Dow m) (A_Dow n)

theorem infiniteA_Dow {n : ℕ} : Infinite ↑(A_Dow n)

def almost_disjoint (B : Set ℕ) (C : ℕ → Set ℕ) : Set ℕ

Equations

• almost_disjoint B C n = Finite ↑((C n).inter B)

def Abot : Set (Set ℕ)

Equations

• Abot B = (almost_disjoint B A_Dow = Set.univ)

def I_Dow : Set (Set ℕ)

Equations

• I_Dow B = ∃ (n₀ : ℕ), ∀ (n : ℕ), n₀ ≤ n → n ∈ almost_disjoint B A_Dow

theorem AbotI_Dow_contained : Abot ⊆ I_Dow