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_exists_closure_subset [NormalSpace X] {s t : Set X} (hs : IsClosed s) (ht : IsOpen t) (hst : s ⊆ t) :
∃ u, IsOpen u ∧ s ⊆ u ∧ closure u ⊆ t :=
by
have : Disjoint s tᶜ := Set.disjoint_left.mpr fun x hxs hxt => hxt (hst hxs)
rcases normal_separation hs (isClosed_compl_iff.2 ht) this with ⟨s', t', hs', ht', hss', htt', hs't'⟩
refine ⟨s', hs', hss', Subset.trans (closure_minimal ?_ (isClosed_compl_iff.2 ht')) (compl_subset_comm.1 htt')⟩
exact fun x hxs hxt => hs't'.le_bot ⟨hxs, hxt⟩
