exists_subset_nhds_of_compactSpace

English

In a compact space X, for a directed family of closed sets V_i, every neighborhood-coverage condition implies the existence of some i with V_i ⊆ U.

Русский

В компактном пространстве X по направленной семье закрытых множеств V_i существование i с V_i ⊆ U следует из условия, что U содержит ⋂_i V_i.

LaTeX

$$Exists i, V_i ⊆ U$$

Lean4

theorem exists_subset_nhds_of_compactSpace [CompactSpace X] [Nonempty ι] {V : ι → Set X} (hV : Directed (· ⊇ ·) V)
    (hV_closed : ∀ i, IsClosed (V i)) {U : Set X} (hU : ∀ x ∈ ⋂ i, V i, U ∈ 𝓝 x) : ∃ i, V i ⊆ U :=
  exists_subset_nhds_of_isCompact' hV (fun i => (hV_closed i).isCompact) hV_closed hU

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