Documentation

Mathlib.Topology.Perfect

Perfect Sets #

In this file we define perfect subsets of a topological space, and prove some basic properties, including a version of the Cantor-Bendixson Theorem.

Main Definitions #

Main Statements #

Implementation Notes #

We do not require perfect sets to be nonempty.

We define a nonstandard predicate, Preperfect, which drops the closed-ness requirement from the definition of perfect. In T1 spaces, this is equivalent to having a perfect closure, see preperfect_iff_perfect_closure.

See also #

Mathlib.Topology.MetricSpace.Perfect, for properties of perfect sets in metric spaces, namely Polish spaces.

References #

Tags #

accumulation point, perfect set, cantor-bendixson.

source
theorem AccPt.nhds_inter {α : Type u_1} [TopologicalSpace α] {C : Set α} {x : α} {U : Set α} (h_acc : AccPt x (Filter.principal C)) (hU : U ∈ nhds x) :
AccPt x (Filter.principal (U ∩ C))

If x is an accumulation point of a set C and U is a neighborhood of x, then x is an accumulation point of U ∩ C.

source
def Preperfect {α : Type u_1} [TopologicalSpace α] (C : Set α) :
Prop

A set C is preperfect if all of its points are accumulation points of itself. If C is nonempty and α is a T1 space, this is equivalent to the closure of C being perfect. See preperfect_iff_perfect_closure.

Equations
Instances For
    source
    structure Perfect {α : Type u_1} [TopologicalSpace α] (C : Set α) :
    Prop

    A set C is called perfect if it is closed and all of its points are accumulation points of itself. Note that we do not require C to be nonempty.

    Instances For
      source
      theorem perfect_def {α : Type u_1} [TopologicalSpace α] (C : Set α) :
      Perfect C ↔ IsClosed C ∧ Preperfect C
      source
      theorem preperfect_iff_nhds {α : Type u_1} [TopologicalSpace α] {C : Set α} :
      Preperfect C ↔ ∀ x ∈ C, ∀ U ∈ nhds x, ∃ y ∈ U ∩ C, y ≠ x
      source
      class PerfectSpace (α : Type u_1) [TopologicalSpace α] :
      Prop

      A topological space X is said to be perfect if its universe is a perfect set. Equivalently, this means that 𝓝[≠] x ≠ ⊥ for every point x : X.

      Instances
        source
        theorem perfectSpace_def (α : Type u_1) [TopologicalSpace α] :
        PerfectSpace α ↔ Preperfect Set.univ
        source
        theorem PerfectSpace.univ_perfect (α : Type u_1) [TopologicalSpace α] [PerfectSpace α] :
        Perfect Set.univ
        source
        theorem Preperfect.open_inter {α : Type u_1} [TopologicalSpace α] {C U : Set α} (hC : Preperfect C) (hU : IsOpen U) :
        Preperfect (U ∩ C)

        The intersection of a preperfect set and an open set is preperfect.

        source
        theorem Preperfect.perfect_closure {α : Type u_1} [TopologicalSpace α] {C : Set α} (hC : Preperfect C) :
        Perfect (closure C)

        The closure of a preperfect set is perfect. For a converse, see preperfect_iff_perfect_closure.

        source
        theorem preperfect_iff_perfect_closure {α : Type u_1} [TopologicalSpace α] {C : Set α} [T1Space α] :
        Preperfect C ↔ Perfect (closure C)

        In a T1 space, being preperfect is equivalent to having perfect closure.

        source
        theorem Perfect.closure_nhds_inter {α : Type u_1} [TopologicalSpace α] {C U : Set α} (hC : Perfect C) (x : α) (xC : x ∈ C) (xU : x ∈ U) (Uop : IsOpen U) :
        Perfect (closure (U ∩ C)) ∧ (closure (U ∩ C)).Nonempty
        source
        theorem Perfect.splitting {α : Type u_1} [TopologicalSpace α] {C : Set α} [T25Space α] (hC : Perfect C) (hnonempty : C.Nonempty) :
        ∃ (C₀ : Set α) (C₁ : Set α), (Perfect C₀ ∧ C₀.Nonempty ∧ C₀ ⊆ C) ∧ (Perfect C₁ ∧ C₁.Nonempty ∧ C₁ ⊆ C) ∧ Disjoint C₀ C₁

        Given a perfect nonempty set in a T2.5 space, we can find two disjoint perfect subsets. This is the main inductive step in the proof of the Cantor-Bendixson Theorem.

        source
        theorem IsPreconnected.preperfect_of_nontrivial {α : Type u_1} [TopologicalSpace α] [T1Space α] {U : Set α} (hu : U.Nontrivial) (h : IsPreconnected U) :
        Preperfect U
        source
        theorem exists_countable_union_perfect_of_isClosed {α : Type u_1} [TopologicalSpace α] {C : Set α} [SecondCountableTopology α] (hclosed : IsClosed C) :
        ∃ (V : Set α) (D : Set α), V.Countable ∧ Perfect D ∧ C = V ∪ D

        The Cantor-Bendixson Theorem: Any closed subset of a second countable space can be written as the union of a countable set and a perfect set.

        source
        theorem exists_perfect_nonempty_of_isClosed_of_not_countable {α : Type u_1} [TopologicalSpace α] {C : Set α} [SecondCountableTopology α] (hclosed : IsClosed C) (hunc : ¬C.Countable) :
        ∃ (D : Set α), Perfect D ∧ D.Nonempty ∧ D ⊆ C

        Any uncountable closed set in a second countable space contains a nonempty perfect subset.

        source
        theorem perfectSpace_iff_forall_not_isolated {X : Type u_1} [TopologicalSpace X] :
        PerfectSpace X ↔ ∀ (x : X), (nhdsWithin x {x}ᶜ).NeBot
        source
        instance PerfectSpace.not_isolated {X : Type u_1} [TopologicalSpace X] [PerfectSpace X] (x : X) :
        (nhdsWithin x {x}ᶜ).NeBot