elim_nhds_subcover' — Mathlib

English

A variant of subcover for nhds with a cofinal family indexed by s.

Русский

Вариант подпокрытия nhds с когениральной семействой, индексируемой по s.

LaTeX

$$$IsCompact(s) \rightarrow \forall U : (x:X) \to Set{x \in s}, 𝓝 x \Rightarrow \exists t : Finset s, s \subseteq \bigcup_{x \in t} U x hx$$$

Lean4

theorem elim_nhds_subcover' (hs : IsCompact s) (U : ∀ x ∈ s, Set X) (hU : ∀ x (hx : x ∈ s), U x ‹x ∈ s› ∈ 𝓝 x) :
    ∃ t : Finset s, s ⊆ ⋃ x ∈ t, U (x : s) x.2 :=
  (hs.elim_nhds_subcover_nhdsSet' U hU).imp fun _ ↦ subset_of_mem_nhdsSet

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