nonempty' — Mathlib

English

In a nonempty locally compact space α, there exists a nonempty PositiveCompacts α.

Русский

В непустом локально компактном пространстве α существует непустой положительный компакт.

LaTeX

$$$\exists K \in PositiveCompacts(\alpha)$$$

Lean4

/-- In a nonempty locally compact space, there exists a compact set with nonempty interior. -/
instance nonempty' [WeaklyLocallyCompactSpace α] [Nonempty α] : Nonempty (PositiveCompacts α) :=
  by
  inhabit α
  rcases exists_compact_mem_nhds (default : α) with ⟨K, hKc, hK⟩
  exact ⟨⟨K, hKc⟩, _, mem_interior_iff_mem_nhds.2 hK⟩

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