closure_eq_self_union_derivedSet

Mathlib.Topology.DerivedSet

URI: https://scilib.ai/kg/mathlib#closure_eq_self_union_derivedSet

← MathLib Explorer

English

closure(A) = A ∪ derivedSet(A).

Русский

Замыкание(A) равно A объединённому с derivedSet(A).

LaTeX

$$$$\overline{A} = A \cup \operatorname{derivedSet}(A).$$$$

Lean4

theorem closure_eq_self_union_derivedSet (A : Set X) : closure A = A ∪ derivedSet A :=
  by
  ext
  simp [closure_eq_cluster_pts, clusterPt_principal]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru