exists_positiveCompacts_closure_subset

English

In an R1 space that is locally compact, for every nonempty open set U there exists a positive compact subset K with closure(K) ⊆ U.

Русский

В пространстве R1, локально компактном, для каждого непустого открытого множества U существует положительное компактное множество K такое, что замыкание(K) ⊆ U.

LaTeX

$$$\exists K \in PositiveCompacts(α), \overline{\uparrow K} \subseteq U$$$

Lean4

theorem _root_.IsOpen.exists_positiveCompacts_closure_subset [R1Space α] [LocallyCompactSpace α] {U : Set α}
    (ho : IsOpen U) (hn : U.Nonempty) : ∃ K : PositiveCompacts α, closure ↑K ⊆ U :=
  let ⟨K, hKU⟩ := exists_positiveCompacts_subset ho hn
  ⟨K, K.isCompact.closure_subset_of_isOpen ho hKU⟩

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