English
If s and t are disjoint from closure t, then ordT5Nhd s t is a neighborhood of s.
Русский
Если s и t дисколированы от замыкания t, то ordT5Nhd s t является окрестностью s.
LaTeX
$$$(Disjoint\ s\ (closure\ t)) \Rightarrow ordT5Nhd\ s\ t \in 𝓝ˢ\ s.$$$
Lean4
theorem ordT5Nhd_mem_nhdsSet (hd : Disjoint s (closure t)) : ordT5Nhd s t ∈ 𝓝ˢ s :=
bUnion_mem_nhdsSet fun x hx =>
ordConnectedComponent_mem_nhds.2 <|
inter_mem
(by
rw [← mem_interior_iff_mem_nhds, interior_compl]
exact disjoint_left.1 hd hx)
(compl_ordConnectedSection_ordSeparatingSet_mem_nhds hd hx)