ordT5Nhd_mem_nhdsSet — Mathlib

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)

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