English
In such spaces, U is compact and open if and only if U is a finite union of basis elements.
Русский
В таких пространствах U компактно и открыто тогда и только тогда, когда U является конечным объединением элементов базиса.
LaTeX
$$$ IsCompact U \land IsOpen U \iff \exists s, s.Finite \land U = \bigcup i \in s, b i $$$
Lean4
/-- 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) :
IsCompact 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 _)
