[GOAL]
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a b c : X
s t : Set X
⊢ ordConnectedComponent s a ∈ 𝓝 a ↔ s ∈ 𝓝 a
[PROOFSTEP]
refine' ⟨fun h => mem_of_superset h ordConnectedComponent_subset, fun h => _⟩
[GOAL]
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a b c : X
s t : Set X
h : s ∈ 𝓝 a
⊢ ordConnectedComponent s a ∈ 𝓝 a
[PROOFSTEP]
rcases exists_Icc_mem_subset_of_mem_nhds h with ⟨b, c, ha, ha', hs⟩
[GOAL]
case intro.intro.intro.intro
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a b✝ c✝ : X
s t : Set X
h : s ∈ 𝓝 a
b c : X
ha : a ∈ Icc b c
ha' : Icc b c ∈ 𝓝 a
hs : Icc b c ⊆ s
⊢ ordConnectedComponent s a ∈ 𝓝 a
[PROOFSTEP]
exact mem_of_superset ha' (subset_ordConnectedComponent ha hs)
[GOAL]
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))ᶜ ∈ 𝓝[Ici a] a
[PROOFSTEP]
have hmem : tᶜ ∈ 𝓝[≥] a := by
  refine' mem_nhdsWithin_of_mem_nhds _
  rw [← mem_interior_iff_mem_nhds, interior_compl]
  exact disjoint_left.1 hd ha
[GOAL]
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
⊢ tᶜ ∈ 𝓝[Ici a] a
[PROOFSTEP]
refine' mem_nhdsWithin_of_mem_nhds _
[GOAL]
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
⊢ tᶜ ∈ 𝓝 a
[PROOFSTEP]
rw [← mem_interior_iff_mem_nhds, interior_compl]
[GOAL]
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
⊢ a ∈ (closure t)ᶜ
[PROOFSTEP]
exact disjoint_left.1 hd ha
[GOAL]
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
hmem : tᶜ ∈ 𝓝[Ici a] a
⊢ (ordConnectedSection (ordSeparatingSet s t))ᶜ ∈ 𝓝[Ici a] a
[PROOFSTEP]
rcases exists_Icc_mem_subset_of_mem_nhdsWithin_Ici hmem with ⟨b, hab, hmem', hsub⟩
[GOAL]
case intro.intro.intro
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
hmem : tᶜ ∈ 𝓝[Ici a] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[Ici a] a
hsub : Icc a b ⊆ tᶜ
⊢ (ordConnectedSection (ordSeparatingSet s t))ᶜ ∈ 𝓝[Ici a] a
[PROOFSTEP]
by_cases H : Disjoint (Icc a b) (ordConnectedSection <| ordSeparatingSet s t)
[GOAL]
case pos
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
hmem : tᶜ ∈ 𝓝[Ici a] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[Ici a] a
hsub : Icc a b ⊆ tᶜ
H : Disjoint (Icc a b) (ordConnectedSection (ordSeparatingSet s t))
⊢ (ordConnectedSection (ordSeparatingSet s t))ᶜ ∈ 𝓝[Ici a] a
[PROOFSTEP]
exact mem_of_superset hmem' (disjoint_left.1 H)
[GOAL]
case neg
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
hmem : tᶜ ∈ 𝓝[Ici a] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[Ici a] a
hsub : Icc a b ⊆ tᶜ
H : ¬Disjoint (Icc a b) (ordConnectedSection (ordSeparatingSet s t))
⊢ (ordConnectedSection (ordSeparatingSet s t))ᶜ ∈ 𝓝[Ici a] a
[PROOFSTEP]
simp only [Set.disjoint_left, not_forall, Classical.not_not] at H 
[GOAL]
case neg
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
hmem : tᶜ ∈ 𝓝[Ici a] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[Ici a] a
hsub : Icc a b ⊆ tᶜ
H : ∃ x h, x ∈ ordConnectedSection (ordSeparatingSet s t)
⊢ (ordConnectedSection (ordSeparatingSet s t))ᶜ ∈ 𝓝[Ici a] a
[PROOFSTEP]
rcases H with ⟨c, ⟨hac, hcb⟩, hc⟩
[GOAL]
case neg.intro.intro.intro
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
hmem : tᶜ ∈ 𝓝[Ici a] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[Ici a] a
hsub : Icc a b ⊆ tᶜ
c : X
hc : c ∈ ordConnectedSection (ordSeparatingSet s t)
hac : a ≤ c
hcb : c ≤ b
⊢ (ordConnectedSection (ordSeparatingSet s t))ᶜ ∈ 𝓝[Ici a] a
[PROOFSTEP]
have hsub' : Icc a b ⊆ ordConnectedComponent tᶜ a := subset_ordConnectedComponent (left_mem_Icc.2 hab) hsub
[GOAL]
case neg.intro.intro.intro
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
hmem : tᶜ ∈ 𝓝[Ici a] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[Ici a] a
hsub : Icc a b ⊆ tᶜ
c : X
hc : c ∈ ordConnectedSection (ordSeparatingSet s t)
hac : a ≤ c
hcb : c ≤ b
hsub' : Icc a b ⊆ ordConnectedComponent tᶜ a
⊢ (ordConnectedSection (ordSeparatingSet s t))ᶜ ∈ 𝓝[Ici a] a
[PROOFSTEP]
have hd : Disjoint s (ordConnectedSection (ordSeparatingSet s t)) :=
  disjoint_left_ordSeparatingSet.mono_right ordConnectedSection_subset
[GOAL]
case neg.intro.intro.intro
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
hmem : tᶜ ∈ 𝓝[Ici a] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[Ici a] a
hsub : Icc a b ⊆ tᶜ
c : X
hc : c ∈ ordConnectedSection (ordSeparatingSet s t)
hac : a ≤ c
hcb : c ≤ b
hsub' : Icc a b ⊆ ordConnectedComponent tᶜ a
hd : Disjoint s (ordConnectedSection (ordSeparatingSet s t))
⊢ (ordConnectedSection (ordSeparatingSet s t))ᶜ ∈ 𝓝[Ici a] a
[PROOFSTEP]
replace hac : a < c := hac.lt_of_ne <| Ne.symm <| ne_of_mem_of_not_mem hc <| disjoint_left.1 hd ha
[GOAL]
case neg.intro.intro.intro
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
hmem : tᶜ ∈ 𝓝[Ici a] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[Ici a] a
hsub : Icc a b ⊆ tᶜ
c : X
hc : c ∈ ordConnectedSection (ordSeparatingSet s t)
hcb : c ≤ b
hsub' : Icc a b ⊆ ordConnectedComponent tᶜ a
hd : Disjoint s (ordConnectedSection (ordSeparatingSet s t))
hac : a < c
⊢ (ordConnectedSection (ordSeparatingSet s t))ᶜ ∈ 𝓝[Ici a] a
[PROOFSTEP]
refine' mem_of_superset (Ico_mem_nhdsWithin_Ici (left_mem_Ico.2 hac)) fun x hx hx' => _
[GOAL]
case neg.intro.intro.intro
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
hmem : tᶜ ∈ 𝓝[Ici a] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[Ici a] a
hsub : Icc a b ⊆ tᶜ
c : X
hc : c ∈ ordConnectedSection (ordSeparatingSet s t)
hcb : c ≤ b
hsub' : Icc a b ⊆ ordConnectedComponent tᶜ a
hd : Disjoint s (ordConnectedSection (ordSeparatingSet s t))
hac : a < c
x : X
hx : x ∈ Ico a c
hx' : x ∈ ordConnectedSection (ordSeparatingSet s t)
⊢ False
[PROOFSTEP]
refine' hx.2.ne (eq_of_mem_ordConnectedSection_of_uIcc_subset hx' hc _)
[GOAL]
case neg.intro.intro.intro
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
hmem : tᶜ ∈ 𝓝[Ici a] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[Ici a] a
hsub : Icc a b ⊆ tᶜ
c : X
hc : c ∈ ordConnectedSection (ordSeparatingSet s t)
hcb : c ≤ b
hsub' : Icc a b ⊆ ordConnectedComponent tᶜ a
hd : Disjoint s (ordConnectedSection (ordSeparatingSet s t))
hac : a < c
x : X
hx : x ∈ Ico a c
hx' : x ∈ ordConnectedSection (ordSeparatingSet s t)
⊢ [[x, c]] ⊆ ordSeparatingSet s t
[PROOFSTEP]
refine' subset_inter (subset_iUnion₂_of_subset a ha _) _
[GOAL]
case neg.intro.intro.intro.refine'_1
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
hmem : tᶜ ∈ 𝓝[Ici a] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[Ici a] a
hsub : Icc a b ⊆ tᶜ
c : X
hc : c ∈ ordConnectedSection (ordSeparatingSet s t)
hcb : c ≤ b
hsub' : Icc a b ⊆ ordConnectedComponent tᶜ a
hd : Disjoint s (ordConnectedSection (ordSeparatingSet s t))
hac : a < c
x : X
hx : x ∈ Ico a c
hx' : x ∈ ordConnectedSection (ordSeparatingSet s t)
⊢ [[x, c]] ⊆ ordConnectedComponent tᶜ a
[PROOFSTEP]
exact OrdConnected.uIcc_subset inferInstance (hsub' ⟨hx.1, hx.2.le.trans hcb⟩) (hsub' ⟨hac.le, hcb⟩)
[GOAL]
case neg.intro.intro.intro.refine'_2
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
hmem : tᶜ ∈ 𝓝[Ici a] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[Ici a] a
hsub : Icc a b ⊆ tᶜ
c : X
hc : c ∈ ordConnectedSection (ordSeparatingSet s t)
hcb : c ≤ b
hsub' : Icc a b ⊆ ordConnectedComponent tᶜ a
hd : Disjoint s (ordConnectedSection (ordSeparatingSet s t))
hac : a < c
x : X
hx : x ∈ Ico a c
hx' : x ∈ ordConnectedSection (ordSeparatingSet s t)
⊢ [[x, c]] ⊆ ⋃ (x : X) (_ : x ∈ t), ordConnectedComponent sᶜ x
[PROOFSTEP]
rcases mem_iUnion₂.1 (ordConnectedSection_subset hx').2 with ⟨y, hyt, hxy⟩
[GOAL]
case neg.intro.intro.intro.refine'_2.intro.intro
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
hmem : tᶜ ∈ 𝓝[Ici a] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[Ici a] a
hsub : Icc a b ⊆ tᶜ
c : X
hc : c ∈ ordConnectedSection (ordSeparatingSet s t)
hcb : c ≤ b
hsub' : Icc a b ⊆ ordConnectedComponent tᶜ a
hd : Disjoint s (ordConnectedSection (ordSeparatingSet s t))
hac : a < c
x : X
hx : x ∈ Ico a c
hx' : x ∈ ordConnectedSection (ordSeparatingSet s t)
y : X
hyt : y ∈ t
hxy : x ∈ ordConnectedComponent sᶜ y
⊢ [[x, c]] ⊆ ⋃ (x : X) (_ : x ∈ t), ordConnectedComponent sᶜ x
[PROOFSTEP]
refine' subset_iUnion₂_of_subset y hyt (OrdConnected.uIcc_subset inferInstance hxy _)
[GOAL]
case neg.intro.intro.intro.refine'_2.intro.intro
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
hmem : tᶜ ∈ 𝓝[Ici a] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[Ici a] a
hsub : Icc a b ⊆ tᶜ
c : X
hc : c ∈ ordConnectedSection (ordSeparatingSet s t)
hcb : c ≤ b
hsub' : Icc a b ⊆ ordConnectedComponent tᶜ a
hd : Disjoint s (ordConnectedSection (ordSeparatingSet s t))
hac : a < c
x : X
hx : x ∈ Ico a c
hx' : x ∈ ordConnectedSection (ordSeparatingSet s t)
y : X
hyt : y ∈ t
hxy : x ∈ ordConnectedComponent sᶜ y
⊢ c ∈ ordConnectedComponent sᶜ y
[PROOFSTEP]
refine' subset_ordConnectedComponent left_mem_uIcc hxy _
[GOAL]
case neg.intro.intro.intro.refine'_2.intro.intro
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
hmem : tᶜ ∈ 𝓝[Ici a] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[Ici a] a
hsub : Icc a b ⊆ tᶜ
c : X
hc : c ∈ ordConnectedSection (ordSeparatingSet s t)
hcb : c ≤ b
hsub' : Icc a b ⊆ ordConnectedComponent tᶜ a
hd : Disjoint s (ordConnectedSection (ordSeparatingSet s t))
hac : a < c
x : X
hx : x ∈ Ico a c
hx' : x ∈ ordConnectedSection (ordSeparatingSet s t)
y : X
hyt : y ∈ t
hxy : x ∈ ordConnectedComponent sᶜ y
⊢ c ∈ [[y, x]]
[PROOFSTEP]
suffices c < y by
  rw [uIcc_of_ge (hx.2.trans this).le]
  exact ⟨hx.2.le, this.le⟩
[GOAL]
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
hmem : tᶜ ∈ 𝓝[Ici a] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[Ici a] a
hsub : Icc a b ⊆ tᶜ
c : X
hc : c ∈ ordConnectedSection (ordSeparatingSet s t)
hcb : c ≤ b
hsub' : Icc a b ⊆ ordConnectedComponent tᶜ a
hd : Disjoint s (ordConnectedSection (ordSeparatingSet s t))
hac : a < c
x : X
hx : x ∈ Ico a c
hx' : x ∈ ordConnectedSection (ordSeparatingSet s t)
y : X
hyt : y ∈ t
hxy : x ∈ ordConnectedComponent sᶜ y
this : c < y
⊢ c ∈ [[y, x]]
[PROOFSTEP]
rw [uIcc_of_ge (hx.2.trans this).le]
[GOAL]
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
hmem : tᶜ ∈ 𝓝[Ici a] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[Ici a] a
hsub : Icc a b ⊆ tᶜ
c : X
hc : c ∈ ordConnectedSection (ordSeparatingSet s t)
hcb : c ≤ b
hsub' : Icc a b ⊆ ordConnectedComponent tᶜ a
hd : Disjoint s (ordConnectedSection (ordSeparatingSet s t))
hac : a < c
x : X
hx : x ∈ Ico a c
hx' : x ∈ ordConnectedSection (ordSeparatingSet s t)
y : X
hyt : y ∈ t
hxy : x ∈ ordConnectedComponent sᶜ y
this : c < y
⊢ c ∈ Icc x y
[PROOFSTEP]
exact ⟨hx.2.le, this.le⟩
[GOAL]
case neg.intro.intro.intro.refine'_2.intro.intro
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
hmem : tᶜ ∈ 𝓝[Ici a] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[Ici a] a
hsub : Icc a b ⊆ tᶜ
c : X
hc : c ∈ ordConnectedSection (ordSeparatingSet s t)
hcb : c ≤ b
hsub' : Icc a b ⊆ ordConnectedComponent tᶜ a
hd : Disjoint s (ordConnectedSection (ordSeparatingSet s t))
hac : a < c
x : X
hx : x ∈ Ico a c
hx' : x ∈ ordConnectedSection (ordSeparatingSet s t)
y : X
hyt : y ∈ t
hxy : x ∈ ordConnectedComponent sᶜ y
⊢ c < y
[PROOFSTEP]
refine' lt_of_not_le fun hyc => _
[GOAL]
case neg.intro.intro.intro.refine'_2.intro.intro
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
hmem : tᶜ ∈ 𝓝[Ici a] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[Ici a] a
hsub : Icc a b ⊆ tᶜ
c : X
hc : c ∈ ordConnectedSection (ordSeparatingSet s t)
hcb : c ≤ b
hsub' : Icc a b ⊆ ordConnectedComponent tᶜ a
hd : Disjoint s (ordConnectedSection (ordSeparatingSet s t))
hac : a < c
x : X
hx : x ∈ Ico a c
hx' : x ∈ ordConnectedSection (ordSeparatingSet s t)
y : X
hyt : y ∈ t
hxy : x ∈ ordConnectedComponent sᶜ y
hyc : y ≤ c
⊢ False
[PROOFSTEP]
have hya : y < a := not_le.1 fun hay => hsub ⟨hay, hyc.trans hcb⟩ hyt
[GOAL]
case neg.intro.intro.intro.refine'_2.intro.intro
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
hmem : tᶜ ∈ 𝓝[Ici a] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[Ici a] a
hsub : Icc a b ⊆ tᶜ
c : X
hc : c ∈ ordConnectedSection (ordSeparatingSet s t)
hcb : c ≤ b
hsub' : Icc a b ⊆ ordConnectedComponent tᶜ a
hd : Disjoint s (ordConnectedSection (ordSeparatingSet s t))
hac : a < c
x : X
hx : x ∈ Ico a c
hx' : x ∈ ordConnectedSection (ordSeparatingSet s t)
y : X
hyt : y ∈ t
hxy : x ∈ ordConnectedComponent sᶜ y
hyc : y ≤ c
hya : y < a
⊢ False
[PROOFSTEP]
exact hxy (Icc_subset_uIcc ⟨hya.le, hx.1⟩) ha
[GOAL]
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
[PROOFSTEP]
have hd' : Disjoint (ofDual ⁻¹' s) (closure <| ofDual ⁻¹' t) := hd
[GOAL]
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
[PROOFSTEP]
have ha' : toDual a ∈ ofDual ⁻¹' s := ha
[GOAL]
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
[PROOFSTEP]
simpa only [dual_ordSeparatingSet, dual_ordConnectedSection] using
  compl_section_ordSeparatingSet_mem_nhdsWithin_Ici hd' ha'
[GOAL]
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
[PROOFSTEP]
rw [← nhds_left_sup_nhds_right, mem_sup]
[GOAL]
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
[PROOFSTEP]
exact ⟨compl_section_ordSeparatingSet_mem_nhdsWithin_Iic hd ha, compl_section_ordSeparatingSet_mem_nhdsWithin_Ici hd ha⟩
[GOAL]
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)
x : X
hx : x ∈ s
⊢ tᶜ ∈ 𝓝 x
[PROOFSTEP]
rw [← mem_interior_iff_mem_nhds, interior_compl]
[GOAL]
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)
x : X
hx : x ∈ s
⊢ x ∈ (closure t)ᶜ
[PROOFSTEP]
exact disjoint_left.1 hd hx
