English
In a T1 space, derivedSet(closure A) = derivedSet(A).
Русский
В T1-пространстве derivedSet(closure A) = derivedSet(A).
LaTeX
$$$$\operatorname{derivedSet}(\overline{A}) = \operatorname{derivedSet}(A).$$$$
Lean4
/-- 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`. -/
theorem derivedSet_closure [T1Space X] (A : Set X) : derivedSet (closure A) = derivedSet A :=
by
refine le_antisymm (fun x hx => ?_) (derivedSet_mono _ _ subset_closure)
rw [mem_derivedSet, AccPt, (nhdsWithin_basis_open x { x }ᶜ).inf_principal_neBot_iff] at hx ⊢
peel hx with u hu _
obtain ⟨-, hu_open⟩ := hu
exact mem_closure_iff.mp this.some_mem.2 (u ∩ { x }ᶜ) (hu_open.inter isOpen_compl_singleton) this.some_mem.1
