closure_interior_subset

Mathlib.Topology.Closure

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

English

If s is closed, then closure of interior s is contained in s.

Русский

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

LaTeX

$$$\mathrm{IsClosed}(s) \rightarrow \mathrm{closure}(\mathrm{interior}(s)) \subseteq s$$$

Lean4

theorem closure_interior_subset {s : Set X} (s_closed : IsClosed s) : closure (interior s) ⊆ s :=
  s_closed.closure_subset_iff.mpr interior_subset

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

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

Разделы

Аффилиация

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