English
In a Lindelöf space, for any U assigning a neighborhood to each x, there exists a countable subcollection that still covers X after taking interiors.
Русский
В пространства Линдельфа существует счетное подпокрытие, покрывающее X после взятия interior.
LaTeX
$$$[LindelofSpace X] \{U:X→P(X)\} (hU: \forall x, U(x) \in interior\,(?)) : \exists t:Set X, t.Countable ∧ ⋃_{x∈t} interior(U(x)) = univ$$$
Lean4
theorem countable_cover_nhds_interior [LindelofSpace X] {U : X → Set X} (hU : ∀ x, U x ∈ 𝓝 x) :
∃ t : Set X, t.Countable ∧ ⋃ x ∈ t, interior (U x) = univ :=
let ⟨t, ht⟩ :=
isLindelof_univ.elim_countable_subcover (fun x => interior (U x)) (fun _ => isOpen_interior) fun x _ =>
mem_iUnion.2 ⟨x, mem_interior_iff_mem_nhds.2 (hU x)⟩
⟨t, ⟨ht.1, univ_subset_iff.1 ht.2⟩⟩
