isClosed_of_closure_subset

Mathlib.Topology.Closure

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

English

If closure s is a subset of s, then s is closed.

Русский

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

LaTeX

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

Lean4

theorem isClosed_of_closure_subset (h : closure s ⊆ s) : IsClosed s := by rw [subset_closure.antisymm h];
  exact isClosed_closure

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

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

Разделы

Аффилиация

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