hasBasis_nhdsSet_cthickening — Mathlib

English

If K is compact, the family (nhdsSet K) has a basis of cthickening δ K with δ > 0.

Русский

Если K компактно, у nhdsSet K есть база из cthickening δ K при δ > 0.

LaTeX

$$$ (\\mathcal{N}^{\\mathrm{s}}K).HasBasis (\\delta>0) (\\delta \\mapsto \\mathrm{cthickening}_{\\delta}K).$$$

Lean4

theorem hasBasis_nhdsSet_cthickening {K : Set α} (hK : IsCompact K) :
    (𝓝ˢ K).HasBasis (fun δ : ℝ => 0 < δ) fun δ => cthickening δ K :=
  (hasBasis_nhdsSet K).to_hasBasis' (fun _U hU => hK.exists_cthickening_subset_open hU.1 hU.2) fun _ =>
    cthickening_mem_nhdsSet K

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