Theorems · Theorem · general topology

IsLindelof.disjoint_nhdsSet_left

∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X} {l : Filter X} [CountableInterFilter l],
  IsLindelof s → (Disjoint (nhdsSet s) l ↔ ∀ x ∈ s, Disjoint (nhds x) l)

The neighborhood filter of a Lindelöf set is disjoint with a filter l with the countable intersection property if and only if the neighborhood filter of each point of this set is disjoint with l.

Defined in

Mathlib.Topology.Compactness.Lindelof

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceCountableInterFilter