IsNowhereDense

Mathlib.Topology.GDelta.Basic

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

English

A set s is nowhere dense if the interior of its closure is empty.

Русский

Множество s нигде не плотное тогда и только когда interior(closure(s)) = ∅.

LaTeX

$$$\operatorname{IsNowhereDense}(s) \;\equiv\; \operatorname{int}(\overline{s}) = \emptyset$$$

Lean4

/-- A set is called **nowhere dense** iff its closure has empty interior. -/
def IsNowhereDense (s : Set X) :=
  interior (closure s) = ∅

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

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

Разделы

Аффилиация

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