elim_nhds_subcover_nhdsSet — Mathlib

English

A compact set s admits a finite subcover of neighborhoods indexed by s.

Русский

Компактное множество s имеет конечное подпокрытие окрестностей, индексируемое по s.

LaTeX

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

Lean4

theorem elim_nhds_subcover_nhdsSet (hs : IsCompact s) {U : X → Set X} (hU : ∀ x ∈ s, U x ∈ 𝓝 x) :
    ∃ t : Finset X, (∀ x ∈ t, x ∈ s) ∧ (⋃ x ∈ t, U x) ∈ 𝓝ˢ s :=
  by
  let ⟨t, ht⟩ := hs.elim_nhds_subcover_nhdsSet' (fun x _ => U x) hU
  classical
    exact
    ⟨t.image (↑), fun x hx =>
      let ⟨y, _, hyx⟩ := Finset.mem_image.1 hx
      hyx ▸ y.2,
      by rwa [Finset.set_biUnion_finset_image]⟩

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