Mycielski's theorem

Mycielski's theorem: let X be a nonempty perfect completely metrizable space (for example a nonempty perfect Polish space), and for every n let R n be a meagre set of k n-tuples of points of X. Then there is a continuous injection f of Cantor space ℕ → Bool into X that avoids every R n on injective tuples: whenever a : Fin (k n) → (ℕ → Bool) is injective, the tuple f ∘ a is not in R n.

The binary case says that a meagre subset of X × X misses every pair (f x, f y) with x ≠ y. For the graph of an equivalence relation this produces a Cantor antichain: a meagre equivalence relation on a nonempty perfect completely metrizable space has a continuous injection of Cantor space whose distinct points are inequivalent. This is the last step of the category proof of Silver's theorem, where the pulled-back equivalence relation on Cantor space is shown to be meagre by the Kuratowski–Ulam theorem.

The proof builds a scheme of nonempty open sets indexed by finite binary words, level by level. Each set contains the closures of its two children, which are disjoint and have diameter at most 1 / (j + 1) at level j + 1 (IsOpen.exists_disjoint_closure_subset). After splitting, the sets of the new level are shrunk so that, for every injective tuple of distinct sets of the level, their product lies in finitely many of the dense open sets whose intersection misses R n (TauCeti.exists_forall_univ_pi_subset). Two distinct branches of Cantor space pass through distinct sets from their first difference on (PiNat.eventually_injective_res), so the induced map sends an injective tuple into every one of these dense open sets, hence outside R n. Avoidance holds only in the limit: a dense meagre set meets every product of nonempty open sets, so no finite stage avoids it.

Main results

• TauCeti.mycielski: Mycielski's theorem.
• TauCeti.mycielski_prod: the binary case, for one meagre subset of X × X.
• Setoid.hasCantorAntichainOn_univ_of_isMeagre: a meagre equivalence relation has a Cantor antichain.

References

• J. Mycielski, Independent sets in topological algebras, Fund. Math. 55 (1964), 139–147.
• A. S. Kechris, Classical Descriptive Set Theory, Graduate Texts in Mathematics 156, Springer, 1995, Theorem 19.1.
• The scheme is assembled with Mathlib's CantorScheme.inducedMap, as in Mathlib's proof of Perfect.exists_nat_bool_injection.

theorem TauCeti.mycielski {X : Type u_1} [TopologicalSpace X] [TopologicalSpace.IsCompletelyMetrizableSpace X] [PerfectSpace X] [Nonempty X] (k : ℕ → ℕ) (R : (n : ℕ) → Set (Fin (k n) → X)) (hR : ∀ (n : ℕ), IsMeagre (R n)) : ∃ (f : (ℕ → Bool) → X), Continuous f ∧ Function.Injective f ∧ ∀ (n : ℕ) (a : Fin (k n) → ℕ → Bool), Function.Injective a → f ∘ a ∉ R n

Mycielski's theorem. Let X be a nonempty perfect completely metrizable space, for example a nonempty perfect Polish space, and let R n be a meagre set of k n-tuples of points of X for each n. There is a continuous injection f of Cantor space into X such that for every n and every injective tuple a of k n points of Cantor space, f ∘ a ∉ R n.

theorem TauCeti.mycielski_prod {X : Type u_1} [TopologicalSpace X] [TopologicalSpace.IsCompletelyMetrizableSpace X] [PerfectSpace X] [Nonempty X] {M : Set (X × X)} (hM : IsMeagre M) : ∃ (f : (ℕ → Bool) → X), Continuous f ∧ Function.Injective f ∧ ∀ (x y : ℕ → Bool), x ≠ y → (f x, f y) ∉ M

Mycielski's theorem, binary case. A meagre subset M of X × X, for a nonempty perfect completely metrizable space X, misses every pair (f x, f y) with x ≠ y for some continuous injection f of Cantor space into X.

theorem Setoid.hasCantorAntichainOn_univ_of_isMeagre {X : Type u_1} [TopologicalSpace X] [TopologicalSpace.IsCompletelyMetrizableSpace X] [PerfectSpace X] [Nonempty X] (E : Setoid X) (hE : IsMeagre {p : X × X | E p.1 p.2}) : E.HasCantorAntichainOn Set.univ

A meagre equivalence relation has a Cantor antichain. If the graph of an equivalence relation E on a nonempty perfect completely metrizable space is meagre in X × X, there is a continuous map of Cantor space into X whose distinct points have E-inequivalent images.