isClosed_derivedSet — Mathlib

English

In a T1 space, the derived set of any A is closed.

Русский

В T1-пространстве любое производное множество является замкнутым.

LaTeX

$$$$\text{IsClosed}(\operatorname{derivedSet}(A)).$$$$

Lean4

@[simp]
theorem isClosed_derivedSet [T1Space X] (A : Set X) : IsClosed (derivedSet A) :=
  by
  rw [← derivedSet_closure, isClosed_iff_derivedSet_subset]
  apply derivedSet_mono
  simp [← isClosed_iff_derivedSet_subset]

Похожие утверждения