of_isCompact_isClosed — Mathlib

English

In a regular Lindelöf space, if s is compact and t is closed and they are disjoint, then s and t have disjoint neighborhoods.

Русский

В регулярном Линдельёфовом пространстве, если s компактно и t замкнуто и они не пересекаются, то существуют разделяющие окрестности.

LaTeX

$$$\text{SeparatedNhds}(s,t)$ при условии $\text{IsCompact}(s)$, $\text{IsClosed}(t)$ и $Disjoint(s,t)$$$

Lean4

/-- In a regular space, if a compact set and a closed set are disjoint, then they have disjoint
neighborhoods. -/
theorem of_isCompact_isClosed {s t : Set X} (hs : IsCompact s) (ht : IsClosed t) (hst : Disjoint s t) :
    SeparatedNhds s t := by
  simpa only [separatedNhds_iff_disjoint, hs.disjoint_nhdsSet_left, disjoint_nhds_nhdsSet, ht.closure_eq,
    disjoint_left] using hst

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