disjoint_nhdsSet_nhdsSet — Mathlib

English

In a NormalSpace X, for closed s,t with s ∩ t = ∅, the lifted nhds sets are disjoint:

Русский

В нормальном пространстве X для замкнутых s,t с пустым пересечением, соответствующие множества nhdsSet несоприкасаются.

LaTeX

$$[NormalSpace X] {s t : Set X} (hs : IsClosed s) (ht : IsClosed t) (hd : Disjoint s t) : Disjoint (nhdsSet s) (nhdsSet t).$$

Lean4

theorem disjoint_nhdsSet_nhdsSet [NormalSpace X] {s t : Set X} (hs : IsClosed s) (ht : IsClosed t) (hd : Disjoint s t) :
    Disjoint (𝓝ˢ s) (𝓝ˢ t) :=
  (normal_separation hs ht hd).disjoint_nhdsSet

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