compl_ordConnectedSection_ordSeparatingSet_mem_nhds

English

For hd and ha, the complement of ordConnectedSection(ordSeparatingSet s t) is a neighborhood of a in the standard topology.

Русский

При hd и ha комплемент ordConnectedSection(ordSeparatingSet s t) является окрестностью точки a в стандартной топологии.

LaTeX

$$(ordConnectedSection (ordSeparatingSet s t))^{c} ∈ 𝓝 a$$

Lean4

theorem compl_ordConnectedSection_ordSeparatingSet_mem_nhds (hd : Disjoint s (closure t)) (ha : a ∈ s) :
    (ordConnectedSection <| ordSeparatingSet s t)ᶜ ∈ 𝓝 a :=
  by
  rw [← nhdsLE_sup_nhdsGE, mem_sup]
  exact
    ⟨compl_ordConnectedSection_ordSeparatingSet_mem_nhdsLE hd ha,
      compl_ordConnectedSection_ordSeparatingSet_mem_nhdsGE hd ha⟩

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