codiscrete — Mathlib

English

The codiscrete filter is the filter of open sets with discrete complement, i.e., those whose complements are discrete subspaces.

Русский

Фильтр кодискретности — фильтр открытых множеств с дискретным комплементом.

LaTeX

$$$\text{codiscrete}(X) = \text{codiscreteWithin}(X, X).$$$

Lean4

/-- In any topological space, the open sets with discrete complement form a filter,
defined as the supremum of all punctured neighborhoods.

See `Filter.mem_codiscrete'` for the equivalence. -/
def codiscrete (X : Type*) [TopologicalSpace X] : Filter X :=
  codiscreteWithin Set.univ

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