feat(topology): add basics of perfect sets (#17492)

add a file perfect.lean which contains basic definitions and facts about perfect sets as well as a version of the Cantor-Bendixson theorem. This is intended to build up to a proof of the Borel isomorphism theorem.



Co-authored-by: Rémy Degenne <[email protected]>
Co-authored-by: Felix-Weilacher <[email protected]>
Co-authored-by: RemyDegenne <[email protected]>

src/topology/basic.lean

@@ -771,6 +771,14 @@ eventually_nhds_iff.2 ⟨t, λ x hx, eventually_nhds_iff.2 ⟨t, htp, hto, hx⟩
   (∀ᶠ y in 𝓝 a, ∀ᶠ x in 𝓝 y, p x) ↔ ∀ᶠ x in 𝓝 a, p x :=
 ⟨λ h, h.self_of_nhds, λ h, h.eventually_nhds⟩
 
+@[simp] lemma frequently_frequently_nhds {p : α → Prop} {a : α} :
+  (∃ᶠ y in 𝓝 a, ∃ᶠ x in 𝓝 y, p x) ↔ (∃ᶠ x in 𝓝 a, p x) :=
+begin
+  rw ← not_iff_not,
+  simp_rw not_frequently,
+  exact eventually_eventually_nhds,
+end
+
 @[simp] lemma eventually_mem_nhds {s : set α} {a : α} :
   (∀ᶠ x in 𝓝 a, s ∈ 𝓝 x) ↔ s ∈ 𝓝 a :=
 eventually_eventually_nhds
@@ -938,6 +946,33 @@ begin
   exact ne_bot_of_le this
 end
 
+/--A point `x` is an accumulation point of a filter `F` if `𝓝[≠] x ⊓ F ≠ ⊥`.-/
+def acc_pt (x : α) (F : filter α) : Prop := ne_bot (𝓝[≠] x ⊓ F)
+
+lemma acc_iff_cluster (x : α) (F : filter α) : acc_pt x F ↔ cluster_pt x (𝓟 {x}ᶜ ⊓ F) :=
+by rw [acc_pt, nhds_within, cluster_pt, inf_assoc]
+
+/-- `x` is an accumulation point of a set `C` iff it is a cluster point of `C ∖ {x}`.-/
+lemma acc_principal_iff_cluster (x : α) (C : set α) :
+  acc_pt x (𝓟 C) ↔ cluster_pt x (𝓟(C \ {x})) :=
+by rw [acc_iff_cluster, inf_principal, inter_comm]; refl
+
+/-- `x` is an accumulation point of a set `C` iff every neighborhood
+of `x` contains a point of `C` other than `x`. -/
+lemma acc_pt_iff_nhds (x : α) (C : set α) : acc_pt x (𝓟 C) ↔ ∀ U ∈ 𝓝 x, ∃ y ∈ U ∩ C, y ≠ x :=
+by simp [acc_principal_iff_cluster, cluster_pt_principal_iff, set.nonempty, exists_prop,
+  and_assoc, and_comm (¬ _ = x)]
+
+/-- `x` is an accumulation point of a set `C` iff
+there are points near `x` in `C` and different from `x`.-/
+lemma acc_pt_iff_frequently (x : α) (C : set α) : acc_pt x (𝓟 C) ↔ ∃ᶠ y in 𝓝 x, y ≠ x ∧ y ∈ C :=
+by simp [acc_principal_iff_cluster, cluster_pt_principal_iff_frequently, and_comm]
+
+/-- If `x` is an accumulation point of `F` and `F ≤ G`, then
+`x` is an accumulation point of `D. -/
+lemma acc_pt.mono {x : α} {F G : filter α} (h : acc_pt x F) (hFG : F ≤ G) : acc_pt x G :=
+⟨ne_bot_of_le_ne_bot h.ne (inf_le_inf_left _ hFG)⟩
+
 /-!
 ### Interior, closure and frontier in terms of neighborhoods
 -/

src/topology/perfect.lean

@@ -0,0 +1,213 @@
+/-
+Copyright (c) 2022 Felix Weilacher. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Felix Weilacher
+-/
+import topology.separation
+import topology.bases
+
+/-!
+# 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
+
+* `perfect C`: A set `C` is perfect, meaning it is closed and every point of it
+  is an accumulation point of itself.
+
+## Main Statements
+
+* `perfect.splitting`: A perfect nonempty set contains two disjoint perfect nonempty subsets.
+  The main inductive step in the construction of an embedding from the Cantor space to a
+  perfect nonempty complete metric space.
+* `exists_countable_union_perfect_of_is_closed`: One version of the **Cantor-Bendixson Theorem**:
+  A closed set in a second countable space can be written as the union of a countable set and a
+  perfect set.
+
+## 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`.
+
+## References
+
+* [kechris1995] (Chapter 6)
+
+## Tags
+
+accumulation point, perfect set, Cantor-Bendixson.
+
+-/
+
+open_locale topological_space filter
+open topological_space filter set
+
+variables {α : Type*} [topological_space α] {C : set α}
+
+/-- 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`. -/
+theorem acc_pt.nhds_inter {x : α} {U : set α} (h_acc : acc_pt x (𝓟 C)) (hU : U ∈ 𝓝 x) :
+  acc_pt x (𝓟 (U ∩ C)) :=
+begin
+  have : 𝓝[≠] x ≤ 𝓟 U,
+  { rw le_principal_iff,
+    exact mem_nhds_within_of_mem_nhds hU, },
+  rw [acc_pt, ← inf_principal, ← inf_assoc, inf_of_le_left this],
+  exact h_acc,
+end
+
+/-- 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`.-/
+def preperfect (C : set α) : Prop := ∀ x ∈ C, acc_pt x (𝓟 C)
+
+/-- 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.-/
+structure perfect (C : set α) : Prop :=
+(closed : is_closed C)
+(acc : preperfect C)
+
+lemma preperfect_iff_nhds : preperfect C ↔ ∀ x ∈ C, ∀ U ∈ 𝓝 x, ∃ y ∈ U ∩ C, y ≠ x :=
+by simp only [preperfect, acc_pt_iff_nhds]
+
+/-- The intersection of a preperfect set and an open set is preperfect-/
+theorem preperfect.open_inter {U : set α} (hC : preperfect C) (hU : is_open U) :
+  preperfect (U ∩ C) :=
+begin
+  rintros x ⟨xU, xC⟩,
+  apply (hC _ xC).nhds_inter,
+  exact hU.mem_nhds xU,
+end
+
+/-- The closure of a preperfect set is perfect.
+For a converse, see `preperfect_iff_perfect_closure`-/
+theorem preperfect.perfect_closure (hC : preperfect C) : perfect (closure C) :=
+begin
+  split, { exact is_closed_closure },
+  intros x hx,
+  by_cases h : x ∈ C; apply acc_pt.mono _ (principal_mono.mpr subset_closure),
+  { exact hC _ h },
+  have : {x}ᶜ ∩ C = C := by simp [h],
+  rw [acc_pt, nhds_within, inf_assoc, inf_principal, this],
+  rw [closure_eq_cluster_pts] at hx,
+  exact hx,
+end
+
+/-- In a T1 space, being preperfect is equivalent to having perfect closure.-/
+theorem preperfect_iff_perfect_closure [t1_space α] :
+  preperfect C ↔ perfect (closure C) :=
+begin
+  split; intro h, { exact h.perfect_closure },
+  intros x xC,
+  have H : acc_pt x (𝓟 (closure C)) := h.acc _ (subset_closure xC),
+  rw acc_pt_iff_frequently at *,
+  have : ∀ y , y ≠ x ∧ y ∈ closure C → ∃ᶠ z in 𝓝 y, z ≠ x ∧ z ∈ C,
+  { rintros y ⟨hyx, yC⟩,
+    simp only [← mem_compl_singleton_iff, @and_comm _ (_ ∈ C) , ← frequently_nhds_within_iff,
+      hyx.nhds_within_compl_singleton, ← mem_closure_iff_frequently],
+    exact yC, },
+  rw ← frequently_frequently_nhds,
+  exact H.mono this,
+end
+
+theorem perfect.closure_nhds_inter {U : set α} (hC : perfect C) (x : α) (xC : x ∈ C) (xU : x ∈ U)
+  (Uop : is_open U) : perfect (closure (U ∩ C)) ∧ (closure (U ∩ C)).nonempty :=
+begin
+  split,
+  { apply preperfect.perfect_closure,
+    exact (hC.acc).open_inter Uop, },
+  apply nonempty.closure,
+  exact ⟨x, ⟨xU, xC⟩⟩,
+end
+
+/-- 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-/
+lemma perfect.splitting [t2_5_space α] (hC : perfect C) (hnonempty : C.nonempty) :
+  ∃ C₀ C₁ : set α, (perfect C₀ ∧ C₀.nonempty ∧ C₀ ⊆ C) ∧
+  (perfect C₁ ∧ C₁.nonempty ∧ C₁ ⊆ C) ∧ disjoint C₀ C₁ :=
+begin
+  cases hnonempty with y yC,
+  obtain ⟨x, xC, hxy⟩ : ∃ x ∈ C, x ≠ y,
+  { have := hC.acc _ yC,
+    rw acc_pt_iff_nhds at this,
+    rcases this univ (univ_mem) with ⟨x, xC, hxy⟩,
+    exact ⟨x, xC.2, hxy⟩, },
+  obtain ⟨U, xU, Uop, V, yV, Vop, hUV⟩ := exists_open_nhds_disjoint_closure hxy,
+  use [closure (U ∩ C), closure (V ∩ C)],
+  split; rw ← and_assoc,
+  { refine ⟨hC.closure_nhds_inter x xC xU Uop, _⟩,
+    rw hC.closed.closure_subset_iff,
+    exact inter_subset_right _ _, },
+  split,
+  { refine ⟨hC.closure_nhds_inter y yC yV Vop, _⟩,
+    rw hC.closed.closure_subset_iff,
+    exact inter_subset_right _ _, },
+  apply disjoint.mono _ _ hUV; apply closure_mono; exact inter_subset_left _ _,
+end
+
+section kernel
+
+/-- 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.-/
+theorem exists_countable_union_perfect_of_is_closed [second_countable_topology α]
+  (hclosed : is_closed C) :
+  ∃ V D : set α, (V.countable) ∧ (perfect D) ∧ (C = V ∪ D) :=
+begin
+  obtain ⟨b, bct, bnontrivial, bbasis⟩ := topological_space.exists_countable_basis α,
+  let v := {U ∈ b | (U ∩ C).countable},
+  let V := ⋃ U ∈ v, U,
+  let D := C \ V,
+  have Vct : (V ∩ C).countable,
+  { simp only [Union_inter, mem_sep_iff],
+    apply countable.bUnion,
+    { exact countable.mono (inter_subset_left _ _) bct, },
+    { exact inter_subset_right _ _, }, },
+  refine ⟨V ∩ C, D, Vct, ⟨_, _⟩, _⟩,
+  { refine hclosed.sdiff (is_open_bUnion (λ U, _)),
+    exact λ ⟨Ub, _⟩, is_topological_basis.is_open bbasis Ub, },
+  { rw preperfect_iff_nhds,
+    intros x xD E xE,
+    have : ¬ (E ∩ D).countable,
+    { intro h,
+      obtain ⟨U, hUb, xU, hU⟩ : ∃ U ∈ b, x ∈ U ∧ U ⊆ E,
+      { exact (is_topological_basis.mem_nhds_iff bbasis).mp xE, },
+      have hU_cnt : (U ∩ C).countable,
+      { apply @countable.mono _ _ ((E ∩ D) ∪ (V ∩ C)),
+        { rintros y ⟨yU, yC⟩,
+          by_cases y ∈ V,
+          { exact mem_union_right _ (mem_inter h yC), },
+          { exact mem_union_left _ (mem_inter (hU yU) ⟨yC, h⟩), }, },
+        exact countable.union h Vct, },
+      have : U ∈ v := ⟨hUb, hU_cnt⟩,
+      apply xD.2,
+      exact mem_bUnion this xU, },
+    by_contradiction h,
+    push_neg at h,
+    exact absurd (countable.mono h (set.countable_singleton _)) this, },
+  { rw [inter_comm, inter_union_diff], },
+end
+
+/-- Any uncountable closed set in a second countable space contains a nonempty perfect subset.-/
+theorem exists_perfect_nonempty_of_is_closed_of_not_countable [second_countable_topology α]
+  (hclosed : is_closed C) (hunc : ¬ C.countable) :
+  ∃ D : set α, perfect D ∧ D.nonempty ∧ D ⊆ C :=
+begin
+  rcases exists_countable_union_perfect_of_is_closed hclosed with ⟨V, D, Vct, Dperf, VD⟩,
+  refine ⟨D, ⟨Dperf, _⟩⟩,
+  split,
+  { rw nonempty_iff_ne_empty,
+    by_contradiction,
+    rw [h, union_empty] at VD,
+    rw VD at hunc,
+    contradiction, },
+  rw VD,
+  exact subset_union_right _ _,
+end
+
+end kernel