Module docstring
{"# Topological bases in compact sets and compact spaces "}
isCompact_open_iff_eq_finite_iUnion_of_isTopologicalBasis
theorem
(b : ι → Set X) (hb : 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
Full source
/-- 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 -/
theorem isCompact_open_iff_eq_finite_iUnion_of_isTopologicalBasis (b : ι → Set X)
(hb : IsTopologicalBasis (Set.range b)) (hb' : ∀ i, IsCompact (b i)) (U : Set X) :
IsCompactIsCompact U ∧ IsOpen UIsCompact U ∧ IsOpen U ↔ ∃ s : Set ι, s.Finite ∧ U = ⋃ i ∈ s, b i := by
constructor
· exact fun ⟨h₁, h₂⟩ ↦ eq_finite_iUnion_of_isTopologicalBasis_of_isCompact_open _ hb U h₁ h₂
· rintro ⟨s, hs, rfl⟩
constructor
· exact hs.isCompact_biUnion fun i _ => hb' i
· exact isOpen_biUnion fun i _ => hb.isOpen (Set.mem_range_self _)Informal description
Let $X$ be a topological space with a basis $\{b(i)\}_{i \in \iota}$ consisting of compact open sets. Then a subset $U \subseteq X$ is compact and open if and only if it can be expressed as a finite union of some elements from the basis, i.e., there exists a finite subset $s \subseteq \iota$ such that $U = \bigcup_{i \in s} b(i)$.