Stabilizing countably many Borel maps on a Cantor subcopy

CantorStabilization.exists_subcopy_continuous: given countably many maps g i : (ℕ → Bool) → C i into countable discrete spaces, each with Borel fibres, there is one continuous injective e : (ℕ → Bool) → (ℕ → Bool) along which all the composites g i ∘ e are continuous. (Kechris, CDST 8.38 in spirit: Baire-measurable functions are continuous on a comeager set; here the comeager set is then thinned to a Cantor copy.) The conclusion is continuity of g i ∘ e, not continuity of g i at the points of range e.

This is the natural companion of the Cantor-antichain vocabulary in this directory: a construction that produces a Cantor antichain and then needs countably many pieces of Borel data along it to be continuous may pass to the subcopy e first, uniformly for all of them at once.

Route

• Each fibre g i ⁻¹' {c} differs from an open set U by a meager set — the Baire property of Borel sets, MeasurableSet.residualEq_isOpen.
• The countably many exceptional sets are absorbed into one comeager set G on which every fibre is the trace of its open approximant; G is Borel.
• G is uncountable: a countable subset of Cantor space is meager (Cantor space has no isolated points, cantor_nhdsNE_neBot), and a residual set is not (not_isMeagre_of_mem_residual).
• An uncountable Borel subset of a Polish space contains a continuous injective copy of Cantor space (MeasurableSet.exists_nat_bool_injection_of_not_countable): pass to a finer Polish topology making the set clopen (MeasurableSet.isClopenable), apply the closed-set Cantor injection there, and note that the injection stays continuous for the coarser topology.
• Along that copy every fibre of g i ∘ e is the preimage of an open set.

Implementation notes

• PolishSpace (ℕ → Bool) does not currently synthesize; it is assembled here from the countable-Pi second-countability and complete-metrizability instances and kept local to this file.
• The Borel-set-contains-Cantor-copy lemma is stated for an arbitrary Polish space; Mathlib has only the closed-set form (IsClosed.exists_nat_bool_injection_of_not_countable).

Cantor space has no isolated points

Uncountable Borel sets contain Cantor copies

theorem MeasurableSet.exists_nat_bool_injection_of_not_countable {α : Type u_1} [TopologicalSpace α] [PolishSpace α] [MeasurableSpace α] [BorelSpace α] {s : Set α} (hs : MeasurableSet s) (hunc : ¬s.Countable) : ∃ (f : (ℕ → Bool) → α), Set.range f ⊆ s ∧ Continuous f ∧ Function.Injective f

An uncountable Borel subset of a Polish space contains a continuous injective copy of Cantor space. (Finer Polish topology making the set clopen, then the closed-set Cantor injection; the injection stays continuous for the original, coarser topology.)

The stabilization theorem

theorem CantorStabilization.exists_subcopy_continuous {ι : Type u_1} [Countable ι] {C : ι → Type u_2} [(i : ι) → TopologicalSpace (C i)] [∀ (i : ι), DiscreteTopology (C i)] [∀ (i : ι), Countable (C i)] (g : (i : ι) → (ℕ → Bool) → C i) (hg : ∀ (i : ι) (c : C i), MeasurableSet (g i ⁻¹' {c})) : ∃ (e : (ℕ → Bool) → ℕ → Bool), Continuous e ∧ Function.Injective e ∧ ∀ (i : ι), Continuous (g i ∘ e)

Stabilization on a Cantor subcopy. Countably many maps from Cantor space into countable discrete spaces with Borel fibres become simultaneously continuous after composing with one continuous injective self-map of Cantor space.