# Topological bases in compact sets and compact spaces #

source
theorem eq_finite_iUnion_of_isTopologicalBasis_of_isCompact_open {X : Type u_1} {ι : Type u_2} [TopologicalSpace X] (b : ι → Set X) (hb : TopologicalSpace.IsTopologicalBasis (Set.range b)) (U : Set X) (hUc : IsCompact U) (hUo : IsOpen U) :
∃ (s : Set ι), s.Finite ∧ U = ⋃ i ∈ s, b i
source
theorem eq_sUnion_finset_of_isTopologicalBasis_of_isCompact_open {X : Type u_1} [TopologicalSpace X] (b : Set (Set X)) (hb : TopologicalSpace.IsTopologicalBasis b) (U : Set X) (hUc : IsCompact U) (hUo : IsOpen U) :
∃ (s : Finset ↑b), U = ⋃₀ (Subtype.val '' ↑s)
source
theorem isCompact_open_iff_eq_finite_iUnion_of_isTopologicalBasis {X : Type u_1} {ι : Type u_2} [TopologicalSpace X] (b : ι → Set X) (hb : TopologicalSpace.IsTopologicalBasis (Set.range b)) (hb' : ∀ (i : ι), IsCompact (b i)) (U : Set X) :
IsCompact U ∧ IsOpen U ↔ ∃ (s : Set ι), 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