exists_isCompact_cthickening — Mathlib

English

If s is compact, there exists δ > 0 such that cthickening δ s is compact.

Русский

Если s компактно, существует δ > 0 такое, что cthickening δ s компактно.

LaTeX

$$$\\exists \\delta > 0:\\ IsCompact(\\mathrm{cthickening}_{\\delta}(s)).$$$

Lean4

theorem _root_.IsCompact.exists_isCompact_cthickening [LocallyCompactSpace α] (hs : IsCompact s) :
    ∃ δ, 0 < δ ∧ IsCompact (cthickening δ s) :=
  by
  rcases exists_compact_superset hs with ⟨K, K_compact, hK⟩
  rcases hs.exists_cthickening_subset_open isOpen_interior hK with ⟨δ, δpos, hδ⟩
  refine ⟨δ, δpos, ?_⟩
  exact K_compact.of_isClosed_subset isClosed_cthickening (hδ.trans interior_subset)

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