elim_nhdsWithin_subcover — Mathlib

English

A compact set with an nhdsWithin cover has a finite subcover.

Русский

Компактное множество с покрытием nhdsWithin имеет конечное подпокрытие.

LaTeX

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

Lean4

theorem elim_nhdsWithin_subcover (hs : IsCompact s) (U : X → Set X) (hU : ∀ x ∈ s, U x ∈ 𝓝[s] x) :
    ∃ t : Finset X, (∀ x ∈ t, x ∈ s) ∧ s ⊆ ⋃ x ∈ t, U x :=
  by
  choose! V V_nhds hV using fun x hx => mem_nhdsWithin_iff_exists_mem_nhds_inter.1 (hU x hx)
  refine
    (hs.elim_nhds_subcover V V_nhds).imp fun t ⟨t_sub_s, ht⟩ =>
      ⟨t_sub_s, subset_trans ?_ (iUnion₂_mono fun x hx => hV x (t_sub_s x hx))⟩
  simpa [← iUnion_inter]

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