coLindelof — Mathlib

English

The coLindelof filter is generated by complements of Lindelöf sets.

Русский

Фильтр coLindelof задаётся как фильтр, порождаемый дополнениями к множествам Линдельоф.

LaTeX

$$$\mathrm{coLindelof}(X) = \bigwedge_{s\subseteq X,\ IsLindelof(s)} \mathcal{P}(s^c)$$$

Lean4

/-- `Filter.coLindelof` is the filter generated by complements to Lindelöf sets. -/
def coLindelof (X : Type*) [TopologicalSpace X] : Filter X :=
  --`Filter.coLindelof` is the filter generated by complements to Lindelöf sets.

  ⨅ (s : Set X) (_ : IsLindelof s), 𝓟 sᶜ

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