frontier_eq

Mathlib.Topology.Closure

URI: https://scilib.ai/kg/mathlib#IsOpen.frontier_eq

English

Let s be an open set in a topological space X. Then frontier(s) = closure(s) \\ s.

Русский

Пусть s — открытое множество в топологическом пространстве X. Тогда граница s равна замыканию s минус s.

LaTeX

$$$\\operatorname{frontier}(s) = \\overline{s} \\setminus s$$$

Lean4

theorem frontier_eq (hs : IsOpen s) : frontier s = closure s \ s := by rw [frontier, hs.interior_eq]

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

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

Разделы

Аффилиация

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