Derived set

Stream: Is there code for X?

[Daniel Weber]

Is the definition of the derived set of a set somewhere in Mathlib?

[Yury G. Kudryashov]

We have docs#AccPt

[Eric Wieser]

Should that be namespaced within Filter?

[Yury G. Kudryashov]

We have a lot of unresolved issues with namespaces in topology. E.g., some type classes with topology in their names are in the TopologicalSpace NS while docs#Embedding is in the root namespace.

[Yury G. Kudryashov]

If you want to clean up this mess, then I'm ready to quickly review the PRs, but we need to decide what to do with deprecation in refractors like this.

[Daniel Weber]

Yury G. Kudryashov said:

We have docs#AccPt

Yes, I saw that. I proved some lemmas, would this be good to add to Mathlib? Any suggestions?

import Mathlib

open Filter Topology

variable {X : Type*} [TopologicalSpace X]

def DerivedSet (A : Set X) : Set X := {x | AccPt x (𝓟 A)}

lemma derivedSet_union (A B : Set X) : DerivedSet (A ∪ B) = DerivedSet A ∪ DerivedSet B := by
  ext x
  simp only [DerivedSet, accPt_iff_frequently, ne_eq, Set.mem_union, and_or_left,
    frequently_or_distrib, Set.mem_setOf_eq]

lemma derivedSet_mono (A B : Set X) (h : A ⊆ B) : DerivedSet A ⊆ DerivedSet B := by
  intro x hx
  apply AccPt.mono hx
  simp [h]


lemma clusterPt_of_accPt (x : X) (F : Filter X) (h : AccPt x F) : ClusterPt x F := by
  rw [acc_iff_cluster] at h
  apply ClusterPt.mono h
  simp

lemma isClosed_iff_derivedSet_subset (A : Set X) : IsClosed A ↔ DerivedSet A ⊆ A where
  mp h := by
    rw [isClosed_iff_clusterPt] at h
    intro x hx
    apply h
    apply clusterPt_of_accPt
    exact hx
  mpr h := by
    rw [isClosed_iff_clusterPt]
    intro a ha
    by_contra! nh
    have : A = A \ {a} := by simp [nh]
    rw [this, ← acc_principal_iff_cluster] at ha
    exact nh (h ha)

theorem accPt_iff_nhds_open (x : X) (C : Set X) :
      AccPt x (𝓟 C) ↔ ∀ U ∈ 𝓝 x, IsOpen U → ∃ y ∈ U ∩ C, y ≠ x where
  mp h := by
    rw [accPt_iff_nhds] at h
    intros
    apply h
    assumption
  mpr h := by
    rw [accPt_iff_nhds]
    intro U hu
    rw [mem_nhds_iff] at hu
    obtain ⟨t, ht1, ht2, ht3⟩ := hu
    obtain ⟨y, hy1, hy2⟩ := h t (by rw [mem_nhds_iff]; use t) ht2
    use y
    rw [Set.mem_inter_iff] at *
    exact ⟨⟨ht1 hy1.1, hy1.2⟩, hy2⟩

@[simp]
lemma isClosed_derivedSet [T1Space X] (A : Set X) : IsClosed (DerivedSet A) := by
  rw [isClosed_iff_derivedSet_subset]
  intro x hx
  rw [DerivedSet, Set.mem_setOf, accPt_iff_nhds_open] at hx ⊢
  intro U hu1 hu2
  replace hx := hx U hu1 hu2
  obtain ⟨y, hy, h⟩ := hx
  rw [Set.mem_inter_iff] at hy
  obtain ⟨hy1, hy2⟩ := hy
  rw [DerivedSet, Set.mem_setOf, accPt_iff_nhds_open] at hy2
  have : IsOpen (U \ {x}) := IsOpen.sdiff hu2 isClosed_singleton
  obtain ⟨z, hz, -⟩ := hy2 (U \ {x}) (IsOpen.mem_nhds this (by simp [hy1, h])) this
  use z
  simp_all

[Yury G. Kudryashov]

For the last lemma, you don't need T1: docs#isClosed_setOf_clusterPt

[Yury G. Kudryashov]

I don't know whether we need this as a separate definition. @Patrick Massot ?

[Yury G. Kudryashov]

Note that it should be called derivedSet

[Yury G. Kudryashov]

Also, most (all?) of these lemmas have AccPt versions. E.g., it makes sense to add lemmas like clusterPt_sup and accPt_sup.

[Daniel Weber]

Yury G. Kudryashov said:

For the last lemma, you don't need T1: docs#isClosed_setOf_clusterPt

Note that it's the set of AccPts, not ClusterPts, so I do need T1 — the theorem is wrong otherwise

[Yury G. Kudryashov]

:face_palm: You're right, the principal {x}^c part depends on the point.