frontier

Mathlib.Topology.Defs.Basic

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

English

The frontier of s is the boundary: closure(s) minus interior(s).

Русский

Граница s есть граница: closure(s) \ interior(s).

LaTeX

$$$\operatorname{frontier}(s) = \operatorname{closure}(s) \setminus \operatorname{interior}(s)$$$

Lean4

/-- The frontier of a set is the set of points between the closure and interior. -/
def frontier (s : Set X) : Set X :=
  closure s \ interior s

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

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

Разделы

Аффилиация

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