instCompactlyGeneratedSpaceOfWeaklyLocallyCompactSpace

English

A Hausdorff and weakly locally compact space is compactly generated.

Русский

Хаусдорфово и слабо локально компактное пространство — компактно-генерируемое.

LaTeX

$$[WeaklyLocallyCompactSpace X] \\Rightarrow \\text{CompactlyGeneratedSpace}(X)$$

Lean4

/-- A Hausdorff and weakly locally compact space is compactly generated. -/
instance (priority := 100) [WeaklyLocallyCompactSpace X] : CompactlyGeneratedSpace X :=
  by
  refine compactlyGeneratedSpace_of_isClosed_of_t2 fun s h ↦ ?_
  rw [isClosed_iff_forall_filter]
  intro x ℱ hℱ₁ hℱ₂ hℱ₃
  rcases exists_compact_mem_nhds x with ⟨K, hK, K_mem⟩
  exact
    Set.mem_of_mem_inter_left <|
      isClosed_iff_forall_filter.1 (h _ hK) x ℱ hℱ₁
        (Filter.inf_principal ▸ le_inf hℱ₂ (le_trans hℱ₃ <| Filter.le_principal_iff.2 K_mem)) hℱ₃

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