inter_frontier_eq

Mathlib.Topology.Closure

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

English

For an open set s, the intersection of s with its frontier is empty: s ∩ frontier(s) = ∅.

Русский

Для открытого множества s пересечение s и границы(s) пусто: s ∩ frontier(s) = ∅.

LaTeX

$$$\\operatorname{frontier}(s) \\cap s = \emptyset$$$

Lean4

theorem inter_frontier_eq (hs : IsOpen s) : s ∩ frontier s = ∅ := by rw [hs.frontier_eq, inter_diff_self]

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

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

Разделы

Аффилиация

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