closure_discrete

Mathlib.Topology.Order

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

English

In a discrete topology, the closure of a set equals the set itself.

Русский

В дискретной топологии замыкание множества равно самому множеству.

LaTeX

$$$\\overline{A} = A$ for all $A \\subseteq \\alpha$$$

Lean4

theorem closure_discrete (s : Set α) : closure s = s :=
  (isClosed_discrete _).closure_eq

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

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

Разделы

Аффилиация

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