Derived set

This file defines the derived set of a set, the set of all AccPts of its principal filter, and proves some properties of it.

theorem AccPt.map {X : Type u_1} [TopologicalSpace X] {β : Type u_2} [TopologicalSpace β] {F : Filter X} {x : X} (h : AccPt x F) {f : X → β} (hf1 : ContinuousAt f x) (hf2 : Function.Injective f) : AccPt (f x) (Filter.map f F)

def derivedSet {X : Type u_1} [TopologicalSpace X] (A : Set X) : Set X

The derived set of a set is the set of all accumulation points of it.

Equations

• derivedSet A = {x : X | AccPt x (Filter.principal A)}

@[simp]

theorem mem_derivedSet {X : Type u_1} [TopologicalSpace X] {A : Set X} {x : X} : x ∈ derivedSet A ↔ AccPt x (Filter.principal A)

theorem derivedSet_union {X : Type u_1} [TopologicalSpace X] (A B : Set X) : derivedSet (A ∪ B) = derivedSet A ∪ derivedSet B

theorem derivedSet_mono {X : Type u_1} [TopologicalSpace X] (A B : Set X) (h : A ⊆ B) : derivedSet A ⊆ derivedSet B

def relDerivedSet {X : Type u_1} [TopologicalSpace X] : Set X →o Set X

The relative derived set operator viewed as a monotone self-map of Set X.

Equations

• relDerivedSet = { toFun := fun (s : Set X) => derivedSet s ∩ s, monotone' := ⋯ }

@[simp]

theorem relDerivedSet_apply {X : Type u_1} [TopologicalSpace X] (A : Set X) : relDerivedSet A = derivedSet A ∩ A

theorem relDerivedSet_subset {X : Type u_1} [TopologicalSpace X] {A : Set X} : relDerivedSet A ⊆ A

theorem Continuous.image_derivedSet {X : Type u_1} [TopologicalSpace X] {β : Type u_2} [TopologicalSpace β] {A : Set X} {f : X → β} (hf1 : Continuous f) (hf2 : Function.Injective f) : f '' derivedSet A ⊆ derivedSet (f '' A)

theorem derivedSet_subset_closure {X : Type u_1} [TopologicalSpace X] (A : Set X) : derivedSet A ⊆ closure A

theorem isClosed_iff_derivedSet_subset {X : Type u_1} [TopologicalSpace X] (A : Set X) : IsClosed A ↔ derivedSet A ⊆ A

theorem IsClosed.relDerivedSet_eq {X : Type u_1} [TopologicalSpace X] {A : Set X} (hA : IsClosed A) : relDerivedSet A = derivedSet A

theorem closure_eq_self_union_derivedSet {X : Type u_1} [TopologicalSpace X] (A : Set X) : closure A = A ∪ derivedSet A

theorem derivedSet_closure {X : Type u_1} [TopologicalSpace X] [T1Space X] (A : Set X) : derivedSet (closure A) = derivedSet A

In a T1Space, the derivedSet of the closure of a set is equal to the derived set of the set itself.

Note: this doesn't hold in a space with the indiscrete topology. For example, if X is a type with two elements, x and y, and A := {x}, then closure A = Set.univ and derivedSet A = {y}, but derivedSet Set.univ = Set.univ.

@[simp]

theorem isClosed_derivedSet {X : Type u_1} [TopologicalSpace X] [T1Space X] (A : Set X) : IsClosed (derivedSet A)

theorem preperfect_iff_subset_derivedSet {X : Type u_1} [TopologicalSpace X] {U : Set X} : Preperfect U ↔ U ⊆ derivedSet U

theorem preperfect_iff_eq_relDerivedSet {X : Type u_1} [TopologicalSpace X] {U : Set X} : Preperfect U ↔ U = relDerivedSet U

theorem perfect_iff_eq_derivedSet {X : Type u_1} [TopologicalSpace X] {U : Set X} : Perfect U ↔ U = derivedSet U

theorem IsPreconnected.inter_derivedSet_nonempty {X : Type u_1} [TopologicalSpace X] [T1Space X] {U : Set X} (hs : IsPreconnected U) (a b : Set X) (h : U ⊆ a ∪ b) (ha : (U ∩ derivedSet a).Nonempty) (hb : (U ∩ derivedSet b).Nonempty) : (U ∩ (derivedSet a ∩ derivedSet b)).Nonempty