lift'_closure_nhdsSet — Mathlib

English

For any compact K, lifting the closure of nhdsSet K yields nhdsSet K.

Русский

Для компактного K подъем closure nhdsSet K возвращает nhdsSet K.

LaTeX

$$$\forall K:\, IsCompact(K) \Rightarrow ( (nhdsSet(K)).lift' closure = nhdsSet(K) )$$$

Lean4

theorem lift'_closure_nhdsSet {K : Set X} (hK : IsCompact K) : (𝓝ˢ K).lift' closure = 𝓝ˢ K :=
  by
  refine le_antisymm (fun U hU ↦ ?_) (le_lift'_closure _)
  rcases hK.exists_isOpen_closure_subset hU with ⟨V, hVo, hKV, hVU⟩
  exact mem_of_superset (mem_lift' <| hVo.mem_nhdsSet.2 hKV) hVU

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