Theorems · Theorem · general topology

isCompact_open_iff_eq_finite_iUnion_of_isTopologicalBasis

∀ {X : Type u_1} {ι : Type u_2} [inst : TopologicalSpace X] (b : ι → Set X),
  TopologicalSpace.IsTopologicalBasis (Set.range b) →
    (∀ (i : ι), IsCompact (b i)) → ∀ (U : Set X), IsCompact U ∧ IsOpen U ↔ ∃ s, s.Finite ∧ U = ⋃ i ∈ s, b i

If X has a basis consisting of compact opens, then an open set in X is compact open iff it is a finite union of some elements in the basis

Defined in

Mathlib.Topology.Compactness.Bases

Cited by

4 results in Mathlib

Foundations

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

Assumes

TopologicalSpace