residual — Mathlib

English

A set s is called residual if it includes a countable intersection of dense open sets.

Русский

Сосредоточенное резидуальное множество — это множество, содержащее счетное пересечение плотных открытых множеств.

LaTeX

$$$\\text{residual}(X) = \\operatorname{countableGenerate}\\{t\\;|\\; IsOpen(t) \\land Dense(t)\\}$$$

Lean4

/-- A set `s` is called *residual* if it includes a countable intersection of dense open sets. -/
def residual (X : Type*) [TopologicalSpace X] : Filter X :=
  Filter.countableGenerate {t | IsOpen t ∧ Dense t}

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