English
If X has a basis consisting of compact opens, then an open set U is compact and open iff it is a finite union of basis elements: ∃ s, s.Finite ∧ U = ⋃ i ∈ s, b i.
Русский
Если пространство имеет базис из компактных открытых множеств, то открытое множество U компактно и открыто тогда и только тогда, когда оно является конечным объединением элементов базиса.
LaTeX
$$$ IsCompact U \land IsOpen U \iff \exists s : Set \i, s.Finite \land U = \bigcup i \in s, b i $$$
Lean4
theorem eq_finite_iUnion_of_isTopologicalBasis_of_isCompact_open (b : ι → Set X) (hb : IsTopologicalBasis (Set.range b))
(U : Set X) (hUc : IsCompact U) (hUo : IsOpen U) : ∃ s : Set ι, s.Finite ∧ U = ⋃ i ∈ s, b i :=
by
obtain ⟨Y, f, e, hf⟩ := hb.open_eq_iUnion hUo
choose f' hf' using hf
have : b ∘ f' = f := funext hf'
subst this
obtain ⟨t, ht⟩ := hUc.elim_finite_subcover (b ∘ f') (fun i => hb.isOpen (Set.mem_range_self _)) (by rw [e])
classical
refine ⟨t.image f', Set.toFinite _, le_antisymm ?_ ?_⟩
· refine Set.Subset.trans ht ?_
simp only [Set.iUnion_subset_iff]
intro i hi
simpa using subset_iUnion₂ (s := fun i _ => b (f' i)) i hi
· apply Set.iUnion₂_subset
rintro i hi
obtain ⟨j, -, rfl⟩ := Finset.mem_image.mp hi
rw [e]
exact Set.subset_iUnion (b ∘ f') j
