countable_cover_nhds — Mathlib

English

In a Lindelöf space, there exists a countable subfamily t such that ⋃_{x∈t} U(x) = univ for a given U with U(x) ∈ nhds x.

Русский

Для пространства Линдельфа существует счетное подпокрытие, такое что ⋃_{x∈t} U(x) = Univ.

LaTeX

$$$[LindelofSpace X]\{U:X→P(X)\}(hU: ∀ x, U(x) ∈ nhds x) : ∃ t:Set X, t.Countable ∧ ⋃_{x∈t} U(x) = univ$$$

Lean4

theorem countable_cover_nhds [LindelofSpace X] {U : X → Set X} (hU : ∀ x, U x ∈ 𝓝 x) :
    ∃ t : Set X, t.Countable ∧ ⋃ x ∈ t, U x = univ :=
  let ⟨t, ht⟩ := countable_cover_nhds_interior hU
  ⟨t, ⟨ht.1, univ_subset_iff.1 <| ht.2.symm.subset.trans <| iUnion₂_mono fun _ _ => interior_subset⟩⟩

Похожие утверждения