AccPt.nhds_inter
theorem AccPt.nhds_inter :
∀ {α : Type u_1} [inst : TopologicalSpace α] {C : Set α} {x : α} {U : Set α},
AccPt x (Filter.principal C) → U ∈ nhds x → AccPt x (Filter.principal (U ∩ C))
The theorem `AccPt.nhds_inter` states that for any type `α` equipped with a topology, given a set `C`, a point `x` in `α`, and a set `U`, if `x` is an accumulation point of the set `C` (meaning that every neighborhood of `x` contains a point of `C` different from `x`) and `U` is a neighborhood of `x` (meaning it contains an open set around `x`), then `x` is also an accumulation point of the intersection of `U` and `C`. This speaks to the persistence of accumulation points when a neighborhood around them is considered.
More concisely: If a point is an accumulation point of a set and is contained in a neighborhood of another set, then it is also an accumulation point of their intersection.
|
Perfect.splitting
theorem Perfect.splitting :
∀ {α : Type u_1} [inst : TopologicalSpace α] {C : Set α} [inst_1 : T25Space α],
Perfect C →
C.Nonempty →
∃ C₀ C₁, (Perfect C₀ ∧ C₀.Nonempty ∧ C₀ ⊆ C) ∧ (Perfect C₁ ∧ C₁.Nonempty ∧ C₁ ⊆ C) ∧ Disjoint C₀ C₁
The theorem `Perfect.splitting` states that in a T2.5 space, given a perfect (closed with no isolated points) and non-empty set, it is possible to find two disjoint perfect subsets of the given set. These subsets not only have to be perfect and non-empty, but also have to be subsets of the original set. This theorem is a key inductive step in the proof of the Cantor-Bendixson theorem.
More concisely: In a T2.5 space, every perfect and non-empty set contains two disjoint perfect subsets.
|
exists_perfect_nonempty_of_isClosed_of_not_countable
theorem exists_perfect_nonempty_of_isClosed_of_not_countable :
∀ {α : Type u_1} [inst : TopologicalSpace α] {C : Set α} [inst_1 : SecondCountableTopology α],
IsClosed C → ¬C.Countable → ∃ D, Perfect D ∧ D.Nonempty ∧ D ⊆ C
The theorem states that for any uncountable closed set in a second countable topological space, there exists a nonempty perfect subset within that set. Specifically, given a type `α` which has a `TopologicalSpace` structure and an instance of `SecondCountableTopology` on `α`, if `C` is a closed set of `α` which is not countable, then there exists a set `D` which is not only a subset of `C`, but also has the properties of being perfect and nonempty.
Here, a set is perfect if it is closed and contains no isolated points, and a topology is second countable if its topology base has a countable subbase.
More concisely: In a second countable topological space, every uncountable closed set contains a nonempty perfect subset.
|
preperfect_iff_perfect_closure
theorem preperfect_iff_perfect_closure :
∀ {α : Type u_1} [inst : TopologicalSpace α] {C : Set α} [inst_1 : T1Space α], Preperfect C ↔ Perfect (closure C)
This theorem states that in a T1 topological space, a set is preperfect if and only if its closure is perfect. In other words, every point of the set is an accumulation point of the set (making it preperfect) if and only if the closure of the set (the smallest closed set that contains it) contains no isolated points and is closed itself (making it perfect). Here, T1 space refers to a topological space where for each pair of distinct points, each has a neighborhood not containing the other.
More concisely: In a T1 topological space, a set is preperfect if and only if its closure, which is a perfect set, contains no isolated points.
|
exists_countable_union_perfect_of_isClosed
theorem exists_countable_union_perfect_of_isClosed :
∀ {α : Type u_1} [inst : TopologicalSpace α] {C : Set α} [inst_1 : SecondCountableTopology α],
IsClosed C → ∃ V D, V.Countable ∧ Perfect D ∧ C = V ∪ D
The **Cantor-Bendixson Theorem** states that for any closed subset `C` of a type `α`, under the conditions that `α` has a defined topological space and second countable topology, there exist sets `V` and `D` such that `V` is countable, `D` is perfect (i.e., closed and has no isolated points), and `C` is the union of `V` and `D`. This theorem is significant in the field of topology, as it provides a characterization of closed sets in second countable spaces.
More concisely: In any second countable topological space, every closed set is the union of a countable, locally finite open cover and a perfect set.
|
Preperfect.open_inter
theorem Preperfect.open_inter :
∀ {α : Type u_1} [inst : TopologicalSpace α] {C U : Set α}, Preperfect C → IsOpen U → Preperfect (U ∩ C)
The theorem, titled "Preperfect.open_inter", states that for any type `α` that has a topological space structure, and for any two sets `C` and `U` of type `α`, if `C` is a preperfect set and `U` is an open set, then the intersection of `C` and `U` is also a preperfect set. Here, a preperfect set is one where all of its points are accumulation points of itself, and an open set is one that is open in the given topological space structure.
More concisely: If `C` is a preperfect set and `U` is an open set in a topological space, then their intersection `C ∩ U` is also a preperfect set.
|
Preperfect.perfect_closure
theorem Preperfect.perfect_closure :
∀ {α : Type u_1} [inst : TopologicalSpace α] {C : Set α}, Preperfect C → Perfect (closure C)
This theorem states that the closure of a preperfect set is perfect. In the context of topology, a "preperfect" set is defined as one where every point in the set is an accumulation point of the set itself. The "closure" of a set is the smallest closed set that contains the original set. The theorem asserts that if a set is preperfect, then the closure of that set is a "perfect" set. A perfect set, though not explicitly defined in the provided Lean 4 code, typically refers to a closed set with no isolated points. For a reverse implication, one should refer to the `preperfect_iff_perfect_closure` theorem.
More concisely: If a preperfect set in a topological space is closed, then it is a perfect set. (A preperfect set is a set where every point is an accumulation point, and a perfect set is a closed set with no isolated points.)
|