normal_separation — Mathlib

English

In a NormalSpace X, for closed s and open t with s ⊆ t, there exists an open u with s ⊆ u ⊆ closure(u) ⊆ t.

Русский

В нормальном пространстве X, для замкнутого s и открытого t с s ⊆ t существует открытое u такое, что s ⊆ u ⊆ closure(u) ⊆ t.

LaTeX

$$$[NormalSpace X] \land IsClosed(s) \land IsOpen(t) \land s \subseteq t \Rightarrow \exists u, IsOpen(u) \land s \subseteq u \land \overline{u} \subseteq t.$$$

Lean4

theorem normal_separation [NormalSpace X] {s t : Set X} (H1 : IsClosed s) (H2 : IsClosed t) (H3 : Disjoint s t) :
    SeparatedNhds s t :=
  NormalSpace.normal s t H1 H2 H3

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