Theorems · Theorem · general topology

IsCompact.le_nhdsSet_of_clusterPt

∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
  IsCompact s → ∀ {l : Filter X} {s' : Set X}, s ∈ l → (∀ x ∈ s, ClusterPt x l → x ∈ s') → l ≤ nhdsSet s'

If a compact set belongs to a filter and all cluster points in this set and in the filter lie in a set s' then the filter is less than or equal to 𝓝ˢ s'.

Defined in

Mathlib.Topology.Compactness.Compact

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpace