exists_positiveCompacts_subset — Mathlib

English

In a locally compact space α, every nonempty open set U contains a positive compact subset K with K ⊆ U.

Русский

В локально компактном пространстве α любое непустое открытое множество U содержит положительный компактный подмножество K с K ⊆ U.

LaTeX

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

Lean4

theorem _root_.exists_positiveCompacts_subset [LocallyCompactSpace α] {U : Set α} (ho : IsOpen U) (hn : U.Nonempty) :
    ∃ K : PositiveCompacts α, ↑K ⊆ U :=
  let ⟨x, hx⟩ := hn
  let ⟨K, hKc, hxK, hKU⟩ := exists_compact_subset ho hx
  ⟨⟨⟨K, hKc⟩, ⟨x, hxK⟩⟩, hKU⟩

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