elim_nhds_subcover — Mathlib

English

Compactness implies the existence of a finite subcover for nhds when covering by sets.

Русский

Компактность влечет существование конечного подпокрытия для nhds при покрытии множеств.

LaTeX

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

Lean4

theorem elim_nhds_subcover (hs : IsCompact s) (U : X → Set X) (hU : ∀ x ∈ s, U x ∈ 𝓝 x) :
    ∃ t : Finset X, (∀ x ∈ t, x ∈ s) ∧ s ⊆ ⋃ x ∈ t, U x :=
  (hs.elim_nhds_subcover_nhdsSet hU).imp fun _ h ↦ h.imp_right subset_of_mem_nhdsSet

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