Perfect sets: homeomorphic images and products

A homeomorphism carries perfect sets exactly onto perfect sets (Homeomorph.perfect_image), so statements about perfect sets can be transported along homeomorphisms of the ambient spaces.

A product of infinitely many nontrivial topological spaces has no isolated points: a neighbourhood of a point in the product topology constrains only finitely many coordinates, so changing a coordinate outside them moves the point without leaving the neighbourhood. No separation axiom is needed. In particular Cantor space ℕ → Bool and Baire space ℕ → ℕ are perfect.

Main results

• Homeomorph.perfect_image: the image of a set under a homeomorphism is perfect exactly when the set is.
• TauCeti.perfectSpace_pi: a product of infinitely many nontrivial spaces is a perfect space.

References

• The argument for Cantor space follows accPt_univ_natBool in cameronfreer/infinitary-logic at commit 518a366cba97b1ae8c4dc64a297a396939bc3e0b, InfinitaryLogic/Descriptive/PerfectAntichain.lean; here it is stated for arbitrary infinite products of nontrivial spaces.

@[simp]

theorem Homeomorph.perfect_image {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) {C : Set X} : Perfect (⇑h '' C) ↔ Perfect C

The image of a set under a homeomorphism is perfect exactly when the set is perfect.

instance TauCeti.perfectSpace_pi {ι : Type u} {π : ι → Type v} [(i : ι) → TopologicalSpace (π i)] [Infinite ι] [∀ (i : ι), Nontrivial (π i)] : PerfectSpace ((i : ι) → π i)

A product of infinitely many nontrivial spaces is perfect, with no separation assumption on the factors. In particular Cantor space ℕ → Bool and Baire space ℕ → ℕ are perfect.