of_isCompact_isCompact — Mathlib

English

In a Hausdorff space, disjoint compact sets have neighborhoods that separate them in a sense captured by SeparatedNhds.

Русский

В Хаусдорфовом пространстве два несовпадающих компактных множества имеют разделяющие окрестности, выраженные через SeparatedNhds.

LaTeX

$$$[T2Space X]\\; s,t\\subset X\\;\\text{IsCompact } s,IsCompact t,\\;\\text{Disjoint } s\\cap t=\\emptyset\\Rightarrow \\text{SeparatedNhds } s t.$$$

Lean4

theorem of_isCompact_isCompact [T2Space X] {s t : Set X} (hs : IsCompact s) (ht : IsCompact t) (hst : Disjoint s t) :
    SeparatedNhds s t :=
  by
  simp only [SeparatedNhds, prod_subset_compl_diagonal_iff_disjoint.symm] at hst ⊢
  exact generalized_tube_lemma hs ht isClosed_diagonal.isOpen_compl hst

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