Documentation

Mathlib.Topology.DerivedSet

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.

source
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)
source
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
Instances For
    source
    @[simp]
    theorem mem_derivedSet {X : Type u_1} [TopologicalSpace X] {A : Set X} {x : X} :
    x ∈ derivedSet A ↔ AccPt x (Filter.principal A)
    source
    theorem derivedSet_union {X : Type u_1} [TopologicalSpace X] (A : Set X) (B : Set X) :
    derivedSet (A ∪ B) = derivedSet A ∪ derivedSet B
    source
    theorem derivedSet_mono {X : Type u_1} [TopologicalSpace X] (A : Set X) (B : Set X) (h : A ⊆ B) :
    derivedSet A ⊆ derivedSet B
    source
    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)
    source
    theorem derivedSet_subset_closure {X : Type u_1} [TopologicalSpace X] (A : Set X) :
    derivedSet A ⊆ closure A
    source
    theorem isClosed_iff_derivedSet_subset {X : Type u_1} [TopologicalSpace X] (A : Set X) :
    IsClosed A ↔ derivedSet A ⊆ A
    source
    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.

    source
    @[simp]
    theorem isClosed_derivedSet {X : Type u_1} [TopologicalSpace X] [T1Space X] (A : Set X) :
    IsClosed (derivedSet A)
    source
    theorem preperfect_iff_subset_derivedSet {X : Type u_1} [TopologicalSpace X] {U : Set X} :
    Preperfect U ↔ U ⊆ derivedSet U
    source
    theorem perfect_iff_eq_derivedSet {X : Type u_1} [TopologicalSpace X] {U : Set X} :
    Perfect U ↔ U = derivedSet U
    source
    theorem IsPreconnected.inter_derivedSet_nonempty {X : Type u_1} [TopologicalSpace X] [T1Space X] {U : Set X} (hs : IsPreconnected U) (a : Set X) (b : Set X) (h : U ⊆ a ∪ b) (ha : (U ∩ derivedSet a).Nonempty) (hb : (U ∩ derivedSet b).Nonempty) :
    (U ∩ (derivedSet a ∩ derivedSet b)).Nonempty