Topological bases in compact sets and compact spaces

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

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)

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