of_isCompact_isCompact_isClosed — Mathlib

English

If K and L are disjoint compact sets in an R1 space and L is closed, then K and L have disjoint neighborhoods.

Русский

Если K и L раздельны и компактны в R1-пространстве, и L замкнуто, то существуют их раздельные окрестности.

LaTeX

$$SeparatedNhds(K,L)$$

Lean4

/-- If `K` and `L` are disjoint compact sets in an R₁ topological space
and `L` is also closed, then `K` and `L` have disjoint neighborhoods. -/
theorem of_isCompact_isCompact_isClosed {K L : Set X} (hK : IsCompact K) (hL : IsCompact L) (h'L : IsClosed L)
    (hd : Disjoint K L) : SeparatedNhds K L :=
  by
  simp_rw [separatedNhds_iff_disjoint, hK.disjoint_nhdsSet_left, hL.disjoint_nhdsSet_right,
    disjoint_nhds_nhds_iff_not_inseparable]
  intro x hx y hy h
  exact absurd ((h.mem_closed_iff h'L).2 hy) <| disjoint_left.1 hd hx

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