Theorems · Theorem · general topology

UCompactlyGeneratedSpace.isOpen

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

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

Defined in

Mathlib.Topology.Compactness.CompactlyGeneratedSpace

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceUCompactlyGeneratedSpace