hasBasis_nhdsSet_thickening — Mathlib

English

If K is compact, the family (𝓝ˢ K) has a basis consisting of thickening δ K with δ > 0.

Русский

Если K компактно, у семейства (𝓝ˢ K) есть база, состоящая из утолщений δ K при δ > 0.

LaTeX

$$$ (\\mathcal{N}^{\\mathrm{s}}(K)) \\text{ has basis } (\\delta>0) \\mapsto \\mathrm{thickening}_{\\delta}(K).$$$

Lean4

theorem hasBasis_nhdsSet_thickening {K : Set α} (hK : IsCompact K) :
    (𝓝ˢ K).HasBasis (fun δ : ℝ => 0 < δ) fun δ => thickening δ K :=
  (hasBasis_nhdsSet K).to_hasBasis' (fun _U hU => hK.exists_thickening_subset_open hU.1 hU.2) fun _ =>
    thickening_mem_nhdsSet K

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