elim_nhdsWithin_subcover' — Mathlib

English

For nhdsWithin coverings, a finite subcover exists whose members lie within s.

Русский

Для покрытий nhdsWithin существует конечное подпокрытие с членами внутри s.

LaTeX

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

Lean4

theorem elim_nhdsWithin_subcover' (hs : IsCompact s) (U : ∀ x ∈ s, Set X) (hU : ∀ x (hx : x ∈ s), U x hx ∈ 𝓝[s] x) :
    ∃ t : Finset s, s ⊆ ⋃ x ∈ t, U x x.2 :=
  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 ht => subset_trans ?_ (iUnion₂_mono fun x _ => hV x x.2)
  simpa [← iUnion_inter, ← iUnion_coe_set]

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