Theorems · Theorem · general topology

derivedSet_closure

∀ {X : Type u_1} [inst : 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.

Defined in

Mathlib.Topology.DerivedSet

Cited by

1 results in Mathlib

Foundations

Depth 70 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceT1Space