X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a b c : X
s t : Set X
hd : Disjoint s (closure t)
ha : a ∈ s
⊢ ordConnectedSection (ordSeparatingSet s t)ᶜ ∈ 𝓝[Iic a] a ∧ ordConnectedSection (ordSeparatingSet s t)ᶜ ∈ 𝓝[Ici a] a
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a b c : X
s t : Set X
hd : Disjoint s (closure t)
ha : a ∈ s
⊢ ordConnectedSection (ordSeparatingSet s t)ᶜ ∈ 𝓝 a
rw [← nhds_left_sup_nhds_right, mem_sup]
no goals
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a b c : X
s t : Set X
hd : Disjoint s (closure t)
ha : a ∈ s
⊢ ordConnectedSection (ordSeparatingSet s t)ᶜ ∈ 𝓝[Iic a] a ∧ ordConnectedSection (ordSeparatingSet s t)ᶜ ∈ 𝓝[Ici a] a
exact
  ⟨compl_section_ordSeparatingSet_mem_nhdsWithin_Iic hd ha,
    compl_section_ordSeparatingSet_mem_nhdsWithin_Ici hd ha⟩