Transferring category from binary sequences to the real line

Binary expansion is a continuous map from the space of binary sequences onto the unit interval. Each nonempty open set of sequences has an image with nonempty real interior. This suffices to preserve nonmeagreness of images; injectivity and an identification of the spaces are unnecessary.

theorem NonMRR.tendsto_residual_of_image_interior {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) (hf : Continuous f) (himage : ∀ (U : Set X), IsOpen U → U.Nonempty → (interior (f '' U)).Nonempty) : Filter.Tendsto f (residual X) (residual Y)

A continuous map whose nonempty open images have nonempty interior pulls meagre sets back to meagre sets.

theorem NonMRR.nonMeagreCardinal_le_of_tendsto_residual {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] [BaireSpace X] [Nonempty X] (f : X → Y) (hf : Filter.Tendsto f (residual X) (residual Y)) : nonMeagreCardinal Y ≤ nonMeagreCardinal X

Category-preserving maps give the corresponding inequality of uniformities.

theorem NonMRR.binary_ofDigits_image_interior_nonempty (U : Set (ℕ → Fin 2)) (hU : IsOpen U) (hUne : U.Nonempty) : (interior (Real.ofDigits '' U)).Nonempty

Fixing any finite binary prefix still leaves a nondegenerate real interval in its image under binary expansion.

theorem NonMRR.nonM_le_nonMeagreCardinal_finTwo : nonM ≤ nonMeagreCardinal (ℕ → Fin 2)

The literal real uniformity is at most the uniformity on binary digit space.

def NonMRR.boolSequenceHomeomorphFinTwo : (ℕ → Bool) ≃ₜ (ℕ → Fin 2)

The coordinatewise identification of Boolean sequences with binary digits.

Equations

• NonMRR.boolSequenceHomeomorphFinTwo = Homeomorph.piCongrRight fun (x : ℕ) => Homeomorph.ofDiscrete finTwoEquiv.symm

theorem NonMRR.nonM_le_nonMeagreCardinal_bool : nonM ≤ nonMeagreCardinal (ℕ → Bool)

Category on Cantor space bounds category on the actual real line.