English
If X has a basis of compact open sets, then an open set U is Lindelöf and open iff it is a countable union of basis elements.
Русский
Если X имеет базис из компактных открытых множеств, то открытое множество U Линдельоф и открыто тогда, когда его можно представить как счётное объединение элементов базиса.
LaTeX
$$$IsLindelof U \land IsOpen U \iff \exists s : Set\ ι, s.Countable \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 isLindelof_open_iff_eq_countable_iUnion_of_isTopologicalBasis (b : ι → Set X)
(hb : IsTopologicalBasis (Set.range b)) (hb' : ∀ i, IsLindelof (b i)) (U : Set X) :
IsLindelof U ∧ IsOpen U ↔ ∃ s : Set ι, s.Countable ∧ U = ⋃ i ∈ s, b i :=
by
constructor
· rintro ⟨h₁, h₂⟩
obtain ⟨Y, f, rfl, hf⟩ := hb.open_eq_iUnion h₂
choose f' hf' using hf
have : b ∘ f' = f := funext hf'
subst this
obtain ⟨t, ht⟩ := h₁.elim_countable_subcover (b ∘ f') (fun i => hb.isOpen (Set.mem_range_self _)) Subset.rfl
refine ⟨t.image f', Countable.image (ht.1) f', le_antisymm ?_ ?_⟩
· refine Set.Subset.trans ht.2 ?_
simp only [Set.iUnion_subset_iff]
intro i hi
rw [← Set.iUnion_subtype (fun x : ι => x ∈ t.image f') fun i => b i.1]
exact Set.subset_iUnion (fun i : t.image f' => b i) ⟨_, mem_image_of_mem _ hi⟩
· apply Set.iUnion₂_subset
rintro i hi
obtain ⟨j, -, rfl⟩ := (mem_image ..).mp hi
exact Set.subset_iUnion (b ∘ f') j
· rintro ⟨s, hs, rfl⟩
constructor
· exact hs.isLindelof_biUnion fun i _ => hb' i
· exact isOpen_biUnion fun i _ => hb.isOpen (Set.mem_range_self _)
