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
hd' : Disjoint (↑ofDual ⁻¹' s) (closure (↑ofDual ⁻¹' t))
⊢ ordConnectedSection (ordSeparatingSet s t)ᶜ ∈ 𝓝[Iic 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)ᶜ ∈ 𝓝[Iic a] a
have hd' : Disjoint (ofDual ⁻¹' s) (closure <| ofDual ⁻¹' t) := hd
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
hd' : Disjoint (↑ofDual ⁻¹' s) (closure (↑ofDual ⁻¹' t))
ha' : ↑toDual a ∈ ↑ofDual ⁻¹' s
⊢ ordConnectedSection (ordSeparatingSet s t)ᶜ ∈ 𝓝[Iic 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
hd' : Disjoint (↑ofDual ⁻¹' s) (closure (↑ofDual ⁻¹' t))
⊢ ordConnectedSection (ordSeparatingSet s t)ᶜ ∈ 𝓝[Iic a] a
have ha' : toDual a ∈ ofDual ⁻¹' s := ha
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
hd' : Disjoint (↑ofDual ⁻¹' s) (closure (↑ofDual ⁻¹' t))
ha' : ↑toDual a ∈ ↑ofDual ⁻¹' s
⊢ ordConnectedSection (ordSeparatingSet s t)ᶜ ∈ 𝓝[Iic a] a
simpa only [dual_ordSeparatingSet, dual_ordConnectedSection] using
  compl_section_ordSeparatingSet_mem_nhdsWithin_Ici hd' ha'