English
If B is a basis for Opens and U is compact, then there exists a finite subcollection Us ⊆ B such that U is the union of Us.
Русский
Если B является базисом для открытых множеств и U компактно, тогда существует конечная подмножество Us ⊆ B такое, что U равно объединению Us.
LaTeX
$$$\operatorname{IsBasis}(B) \Rightarrow \forall U, \text{IsCompact}(U) \Rightarrow \exists Us \subseteq B, U = \bigcup_{V\in Us} V$$$
Lean4
/-- If `α` has a basis consisting of compact opens, then an open set in `α` is compact open iff
it is a finite union of some elements in the basis -/
theorem isCompact_open_iff_eq_finite_iUnion {ι : Type*} (b : ι → Opens α) (hb : IsBasis (Set.range b))
(hb' : ∀ i, IsCompact (b i : Set α)) (U : Set α) :
IsCompact U ∧ IsOpen U ↔ ∃ s : Set ι, s.Finite ∧ U = ⋃ i ∈ s, b i :=
by
apply isCompact_open_iff_eq_finite_iUnion_of_isTopologicalBasis fun i : ι => (b i).1
· convert (config := { transparency := .default }) hb
ext
simp
· exact hb'
