Finite-block descriptions of meagre sets in Cantor space

This is the topological coding ingredient of the Bartoszyński–Miller characterisation. It does not identify any cardinal invariant by definition.

def NonMRR.replacePrefix (n : ℕ) (s : Fin n → Bool) (x : ℕ → Bool) : ℕ → Bool

Replace the first n coordinates by a prescribed finite word.

Equations

• NonMRR.replacePrefix n s x i = if hi : i < n then s ⟨i, hi⟩ else x i

theorem NonMRR.continuous_replacePrefix (n : ℕ) (s : Fin n → Bool) : Continuous (replacePrefix n s)

theorem NonMRR.dense_preimage_replacePrefix (n : ℕ) (s : Fin n → Bool) {U : Set (ℕ → Bool)} (hU : Dense U) : Dense (replacePrefix n s ⁻¹' U)

Fixing finitely many coordinates pulls a dense set back to a dense set.

theorem NonMRR.exists_tail_block_subset_of_dense_open (n : ℕ) {U : Set (ℕ → Bool)} (hUopen : IsOpen U) (hUdense : Dense U) : ∃ m > n, ∃ (a : ℕ → Bool), ∀ (x : ℕ → Bool), (∀ (i : ℕ), n ≤ i → i < m → x i = a i) → x ∈ U

A dense open subset of Cantor space contains a cylinder determined by a finite block starting at any prescribed coordinate.

theorem NonMRR.meagre_subset_eventually_misses_blocks {M : Set (ℕ → Bool)} (hM : IsMeagre M) : ∃ (g : ℕ → ℕ) (a : ℕ → ℕ → Bool), (∀ (n : ℕ), n < g n) ∧ ∀ x ∈ M, ∀ᶠ (n : ℕ) in Filter.atTop, ¬∀ (i : ℕ), n ≤ i → i < g n → x i = a n i

Every meagre set in Cantor space is contained in a set described by eventual failure to match prescribed finite blocks.

theorem NonMRR.isMeagre_eventually_misses_blocks (g : ℕ → ℕ) (a : ℕ → ℕ → Bool) : IsMeagre {x : ℕ → Bool | ∀ᶠ (n : ℕ) in Filter.atTop, ¬∀ (i : ℕ), n ≤ i → i < g n → x i = a n i}

A set of eventual failures to match blocks is itself meagre.

theorem NonMRR.isMeagre_iff_eventually_misses_blocks {M : Set (ℕ → Bool)} : IsMeagre M ↔ ∃ (g : ℕ → ℕ) (a : ℕ → ℕ → Bool), (∀ (n : ℕ), n < g n) ∧ ∀ x ∈ M, ∀ᶠ (n : ℕ) in Filter.atTop, ¬∀ (i : ℕ), n ≤ i → i < g n → x i = a n i

The finite-block coding characterisation of meagre sets in Cantor space.

theorem NonMRR.exists_pasted_blocks (t : ℕ → ℕ) (ht : StrictMono t) (g : ℕ → ℕ) (a : ℕ → ℕ → Bool) : ∃ (x : ℕ → Bool), ∀ (k : ℕ), g (t k) < t (k + 1) → ∀ (i : ℕ), t k ≤ i → i < g (t k) → x i = a (t k) i

Blocks fitting between consecutive points of a strictly increasing sequence can be pasted into one element of Cantor space.

theorem NonMRR.pasted_blocks_frequently_match {t : ℕ → ℕ} (ht : StrictMono t) {g h : ℕ → ℕ} {a b : ℕ → ℕ → Bool} {x : ℕ → Bool} (hxpaste : ∀ (k : ℕ), g (t k) < t (k + 1) → ∀ (i : ℕ), t k ≤ i → i < g (t k) → x i = a (t k) i) (hmatch : ∃ᶠ (k : ℕ) in Filter.atTop, h (t k) < t (k + 1) ∧ g (t k) = h (t k) ∧ ∀ (i : ℕ), t k ≤ i → i < h (t k) → a (t k) i = b (t k) i) : ∃ᶠ (n : ℕ) in Filter.atTop, ∀ (i : ℕ), n ≤ i → i < h n → x i = b n i

Infinitely many shared fitting blocks force the pasted point outside the meagre set coded by the second collection of blocks.