elim_nhds_subcover — Mathlib

English

In a compact space X, given a function U: X → Set X with U(x) open neighbourhoods of x, there exists a Finset t ⊆ X such that the union over x ∈ t of U(x) covers X.

Русский

В компактном пространстве X дана функция U: X → Set X такая, что U(x) открытое окрестность x; существует конечное подмножество t ⊆ X такое, что ⋃_{x ∈ t} U(x) = X.

LaTeX

$$$\exists t : Finset X, \bigcup_{x \in t} U(x) = ⊤$$$

Lean4

theorem elim_nhds_subcover [CompactSpace X] (U : X → Set X) (hU : ∀ x, U x ∈ 𝓝 x) : ∃ t : Finset X, ⋃ x ∈ t, U x = ⊤ :=
  by
  obtain ⟨t, -, s⟩ := IsCompact.elim_nhds_subcover isCompact_univ U fun x _ => hU x
  exact ⟨t, top_unique s⟩

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