Theorems · Theorem · general topology

UCompactlyGeneratedSpace.isClosed

∀ {X : Type w} [tX : TopologicalSpace X] [UCompactlyGeneratedSpace X] {s : Set X},
  (∀ (S : CompHaus) (f : C(↑S.toTop, X)), IsClosed (⇑f ⁻¹' s)) → IsClosed s

In a compactly generated space X, a set s is closed when f ⁻¹' s is closed for every continuous map f : K → X, where K is compact Hausdorff.

Defined in

Mathlib.Topology.Compactness.CompactlyGeneratedSpace

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceUCompactlyGeneratedSpace