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
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
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
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
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
rcases exists_Icc_mem_subset_of_mem_nhdsWithin_Ici hmem with ⟨b, hab, hmem', hsub⟩
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

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
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
by_cases H : Disjoint (Icc a b) (ordConnectedSection <| ordSeparatingSet s t)
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
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
refine' mem_nhdsWithin_of_mem_nhds _
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ᶜ
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
rw [← mem_interior_iff_mem_nhds, interior_compl]
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
⊢ a ∈ closure tᶜ
exact disjoint_left.1 hd ha
no goals
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
exact mem_of_superset hmem' (disjoint_left.1 H)
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
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
simp only [Set.disjoint_left, not_forall, Classical.not_not] at H
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
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
rcases H with ⟨c, ⟨hac, hcb⟩, hc⟩
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
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
have hsub' : Icc a b ⊆ ordConnectedComponent (tᶜ) a :=
  subset_ordConnectedComponent (left_mem_Icc.2 hab) hsub
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
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
have hd : Disjoint s (ordConnectedSection (ordSeparatingSet s t)) :=
  disjoint_left_ordSeparatingSet.mono_right ordConnectedSection_subset
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
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
replace hac : a < c := hac.lt_of_ne <| Ne.symm <| ne_of_mem_of_not_mem hc <|
  disjoint_left.1 hd ha
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
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
refine' mem_of_superset (Ico_mem_nhdsWithin_Ici (left_mem_Ico.2 hac)) fun x hx hx' => _
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
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
refine' hx.2.ne (eq_of_mem_ordConnectedSection_of_uIcc_subset hx' hc _)
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

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
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
refine' subset_inter (subset_iUnion₂_of_subset a ha _) _
no goals
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
exact OrdConnected.uIcc_subset inferInstance (hsub' ⟨hx.1, hx.2.le.trans hcb⟩)
  (hsub' ⟨hac.le, hcb⟩)
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
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
rcases mem_iUnion₂.1 (ordConnectedSection_subset hx').2 with ⟨y, hyt, hxy⟩
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
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
refine' subset_iUnion₂_of_subset y hyt (OrdConnected.uIcc_subset inferInstance hxy _)
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]]
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
refine' subset_ordConnectedComponent left_mem_uIcc hxy _
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
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]]
suffices c < y by
  rw [uIcc_of_ge (hx.2.trans this).le]
  exact ⟨hx.2.le, this.le⟩
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
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
refine' lt_of_not_le fun hyc => _
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
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
have hya : y < a := not_le.1 fun hay => hsub ⟨hay, hyc.trans hcb⟩ hyt
no goals
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
exact hxy (Icc_subset_uIcc ⟨hya.le, hx.1⟩) ha
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
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]]
rw [uIcc_of_ge (hx.2.trans this).le]
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
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
exact ⟨hx.2.le, this.le⟩