mem_iff_closure_subset

Mathlib.Topology.Closure

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

← MathLib Explorer

English

For a closed s, x ∈ s iff closure {x} ⊆ s.

Русский

Для замкнутого s верно: x ∈ s тогда и только тогда, когда closure {x} ⊆ s.

LaTeX

$$IsClosed(s) \Rightarrow (x \in s \iff \overline{\{x\}} \subseteq s)$$

Lean4

theorem mem_iff_closure_subset (hs : IsClosed s) : x ∈ s ↔ closure ({ x } : Set X) ⊆ s :=
  (hs.closure_subset_iff.trans Set.singleton_subset_iff).symm

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

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

Разделы

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

Аффилиация

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