Theorems · Theorem · general topology

IsLindelof.compl_mem_sets_of_nhdsWithin

∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
  IsLindelof s → ∀ {f : Filter X} [CountableInterFilter f], (∀ x ∈ s, ∃ t ∈ nhdsWithin x s, tᶜ ∈ f) → sᶜ ∈ f

The complement to a Lindelöf set belongs to a filter f with the countable intersection property if each x ∈ s has a neighborhood t within s such that tᶜ belongs to f.

Defined in

Mathlib.Topology.Compactness.Lindelof

Cited by

2 results in Mathlib

Foundations

Depth 75 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceCountableInterFilter