coclosedLindelof — Mathlib

English

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

Русский

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

LaTeX

$$$\mathrm{coclosedLindelof}(X) = \bigwedge_{t:\text{Set }X,\ IsClosed(t),\ IsLindelof(t)} \mathcal{P}(t^c)$$$

Lean4

/-- `Filter.coclosedLindelof` is the filter generated by complements to closed Lindelof sets. -/
def coclosedLindelof (X : Type*) [TopologicalSpace X] : Filter X :=
  -- `Filter.coclosedLindelof` is the filter generated by complements to closed Lindelof sets.

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

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