closure_subset

Mathlib.Topology.Closure

URI: https://scilib.ai/kg/mathlib#IsClosed.closure_subset

English

If s is closed, then closure s ⊆ s.

Русский

Если s замкнуто, то closure s ⊆ s.

LaTeX

$$IsClosed(s) \Rightarrow \overline{s} \subseteq s$$

Lean4

theorem closure_subset (hs : IsClosed s) : closure s ⊆ s :=
  closure_minimal (Subset.refl _) hs

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

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

Разделы

Аффилиация

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