isClosed_iff_derivedSet_subset — Mathlib

English

In any space, IsClosed A is equivalent to derivedSet(A) ⊆ A.

Русский

В любом пространстве IsClosed A эквивалентно тому, что derivedSet(A) ⊆ A.

LaTeX

$$$$\IsClosed(A) \iff \operatorname{derivedSet}(A) \subseteq A.$$$$

Lean4

theorem isClosed_iff_derivedSet_subset (A : Set X) : IsClosed A ↔ derivedSet A ⊆ A
    where
  mp h := derivedSet_subset_closure A |>.trans h.closure_subset
  mpr
    h := by
    rw [isClosed_iff_clusterPt]
    intro a ha
    by_contra! nh
    have : A = A \ { a } := by simp [nh]
    rw [this, ← accPt_principal_iff_clusterPt] at ha
    exact nh (h ha)

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