[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
b : ℤ
⊢ b ≤ ⌊↑(b + 1)⌋
[PROOFSTEP]
rw [floor_intCast]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
b : ℤ
⊢ b ≤ b + 1
[PROOFSTEP]
exact (lt_add_one _).le
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
b : ℤ
⊢ ⌈↑(b - 1)⌉ ≤ b
[PROOFSTEP]
rw [ceil_intCast]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
b : ℤ
⊢ b - 1 ≤ b
[PROOFSTEP]
exact (sub_one_lt _).le
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
n : ℤ
⊢ Tendsto floor (𝓝[Ici ↑n] ↑n) (pure n)
[PROOFSTEP]
simpa only [floor_intCast] using
  tendsto_floor_right_pure_floor
    (n : α)
      -- porting note: new theorem
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
n : ℤ
⊢ Tendsto ceil (𝓝[Iic ↑n] ↑n) (pure n)
[PROOFSTEP]
simpa only [ceil_intCast] using
  tendsto_ceil_left_pure_ceil
    (n : α)
      -- porting note: new theorem
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
x : α
⊢ ↑(⌈x⌉ - 1) < x
[PROOFSTEP]
rw [cast_sub, cast_one, sub_lt_iff_lt_add]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
x : α
⊢ ↑⌈x⌉ < x + 1
[PROOFSTEP]
exact ceil_lt_add_one _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
x : α
h₁ : ↑(⌈x⌉ - 1) < x
⊢ x ≤ ↑(⌈x⌉ - 1) + 1
[PROOFSTEP]
rw [cast_sub, cast_one, sub_add_cancel]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
x : α
h₁ : ↑(⌈x⌉ - 1) < x
⊢ x ≤ ↑⌈x⌉
[PROOFSTEP]
exact le_ceil _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
n : ℤ
⊢ Tendsto floor (𝓝[Iio ↑n] ↑n) (pure (n - 1))
[PROOFSTEP]
simpa only [ceil_intCast] using
  tendsto_floor_left_pure_ceil_sub_one
    (n : α)
      -- porting note: new theorem
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
x : α
⊢ ↑(⌊x⌋ + 1) - 1 ≤ x
[PROOFSTEP]
rw [cast_add, cast_one, add_sub_cancel]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
x : α
⊢ ↑⌊x⌋ ≤ x
[PROOFSTEP]
exact floor_le _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
n : ℤ
⊢ Tendsto ceil (𝓝[Ioi ↑n] ↑n) (pure (n + 1))
[PROOFSTEP]
simpa only [floor_intCast] using tendsto_ceil_right_pure_floor_add_one (n : α)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
n : ℤ
⊢ pure (IntCast.intCast (n - 1)) ≤ 𝓝[Iic (↑n - 1)] (↑n - 1)
[PROOFSTEP]
rw [← @cast_one α, ← cast_sub]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
n : ℤ
⊢ pure (IntCast.intCast (n - 1)) ≤ 𝓝[Iic ↑(n - 1)] ↑(n - 1)
[PROOFSTEP]
exact pure_le_nhdsWithin le_rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
n : ℤ
⊢ pure (IntCast.intCast (n + 1)) ≤ 𝓝[Ici (↑n + 1)] (↑n + 1)
[PROOFSTEP]
rw [← @cast_one α, ← cast_add]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
n : ℤ
⊢ pure (IntCast.intCast (n + 1)) ≤ 𝓝[Ici ↑(n + 1)] ↑(n + 1)
[PROOFSTEP]
exact pure_le_nhdsWithin le_rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : LinearOrderedRing α
inst✝³ : FloorRing α
inst✝² : TopologicalSpace α
inst✝¹ : OrderClosedTopology α
inst✝ : TopologicalAddGroup α
n : ℤ
⊢ Tendsto fract (𝓝[Iio ↑n] ↑n) (𝓝 1)
[PROOFSTEP]
rw [← sub_sub_cancel (n : α) 1]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : LinearOrderedRing α
inst✝³ : FloorRing α
inst✝² : TopologicalSpace α
inst✝¹ : OrderClosedTopology α
inst✝ : TopologicalAddGroup α
n : ℤ
⊢ Tendsto fract (𝓝[Iio ↑n] ↑n) (𝓝 (↑n - (↑n - 1)))
[PROOFSTEP]
refine (tendsto_id.mono_left nhdsWithin_le_nhds).sub ?_
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : LinearOrderedRing α
inst✝³ : FloorRing α
inst✝² : TopologicalSpace α
inst✝¹ : OrderClosedTopology α
inst✝ : TopologicalAddGroup α
n : ℤ
⊢ Tendsto (fun x => ↑⌊x⌋) (𝓝[Iio ↑n] ↑n) (𝓝 (↑n - 1))
[PROOFSTEP]
exact tendsto_floor_left' n
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : LinearOrderedRing α
inst✝⁴ : FloorRing α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : β → α → γ
h : ContinuousOn (uncurry f) (univ ×ˢ Icc 0 1)
hf : ∀ (s : β), f s 0 = f s 1
⊢ Continuous fun st => f st.fst (fract st.snd)
[PROOFSTEP]
change Continuous (uncurry f ∘ Prod.map id fract)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : LinearOrderedRing α
inst✝⁴ : FloorRing α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : β → α → γ
h : ContinuousOn (uncurry f) (univ ×ˢ Icc 0 1)
hf : ∀ (s : β), f s 0 = f s 1
⊢ Continuous (uncurry f ∘ Prod.map id fract)
[PROOFSTEP]
rw [continuous_iff_continuousAt]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : LinearOrderedRing α
inst✝⁴ : FloorRing α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : β → α → γ
h : ContinuousOn (uncurry f) (univ ×ˢ Icc 0 1)
hf : ∀ (s : β), f s 0 = f s 1
⊢ ∀ (x : β × α), ContinuousAt (uncurry f ∘ Prod.map id fract) x
[PROOFSTEP]
rintro ⟨s, t⟩
[GOAL]
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : LinearOrderedRing α
inst✝⁴ : FloorRing α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : β → α → γ
h : ContinuousOn (uncurry f) (univ ×ˢ Icc 0 1)
hf : ∀ (s : β), f s 0 = f s 1
s : β
t : α
⊢ ContinuousAt (uncurry f ∘ Prod.map id fract) (s, t)
[PROOFSTEP]
rcases em (∃ n : ℤ, t = n) with (⟨n, rfl⟩ | ht)
[GOAL]
case mk.inl.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : LinearOrderedRing α
inst✝⁴ : FloorRing α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : β → α → γ
h : ContinuousOn (uncurry f) (univ ×ˢ Icc 0 1)
hf : ∀ (s : β), f s 0 = f s 1
s : β
n : ℤ
⊢ ContinuousAt (uncurry f ∘ Prod.map id fract) (s, ↑n)
[PROOFSTEP]
rw [ContinuousAt, nhds_prod_eq, ← nhds_left'_sup_nhds_right (n : α), prod_sup, tendsto_sup]
[GOAL]
case mk.inl.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : LinearOrderedRing α
inst✝⁴ : FloorRing α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : β → α → γ
h : ContinuousOn (uncurry f) (univ ×ˢ Icc 0 1)
hf : ∀ (s : β), f s 0 = f s 1
s : β
n : ℤ
⊢ Tendsto (uncurry f ∘ Prod.map id fract) (𝓝 s ×ˢ 𝓝[Iio ↑n] ↑n) (𝓝 ((uncurry f ∘ Prod.map id fract) (s, ↑n))) ∧
    Tendsto (uncurry f ∘ Prod.map id fract) (𝓝 s ×ˢ 𝓝[Ici ↑n] ↑n) (𝓝 ((uncurry f ∘ Prod.map id fract) (s, ↑n)))
[PROOFSTEP]
constructor
[GOAL]
case mk.inl.intro.left
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : LinearOrderedRing α
inst✝⁴ : FloorRing α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : β → α → γ
h : ContinuousOn (uncurry f) (univ ×ˢ Icc 0 1)
hf : ∀ (s : β), f s 0 = f s 1
s : β
n : ℤ
⊢ Tendsto (uncurry f ∘ Prod.map id fract) (𝓝 s ×ˢ 𝓝[Iio ↑n] ↑n) (𝓝 ((uncurry f ∘ Prod.map id fract) (s, ↑n)))
[PROOFSTEP]
refine
  (((h (s, 1) ⟨trivial, zero_le_one, le_rfl⟩).tendsto.mono_left ?_).comp
        (tendsto_id.prod_map (tendsto_fract_left _))).mono_right
    (le_of_eq ?_)
[GOAL]
case mk.inl.intro.left.refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : LinearOrderedRing α
inst✝⁴ : FloorRing α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : β → α → γ
h : ContinuousOn (uncurry f) (univ ×ˢ Icc 0 1)
hf : ∀ (s : β), f s 0 = f s 1
s : β
n : ℤ
⊢ 𝓝 s ×ˢ 𝓝[Iio 1] 1 ≤ 𝓝[univ ×ˢ Icc 0 1] (s, 1)
[PROOFSTEP]
rw [nhdsWithin_prod_eq, nhdsWithin_univ, ← nhdsWithin_Ico_eq_nhdsWithin_Iio one_pos]
[GOAL]
case mk.inl.intro.left.refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : LinearOrderedRing α
inst✝⁴ : FloorRing α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : β → α → γ
h : ContinuousOn (uncurry f) (univ ×ˢ Icc 0 1)
hf : ∀ (s : β), f s 0 = f s 1
s : β
n : ℤ
⊢ 𝓝 s ×ˢ 𝓝[Ico 0 1] 1 ≤ 𝓝 s ×ˢ 𝓝[Icc 0 1] 1
[PROOFSTEP]
exact Filter.prod_mono le_rfl (nhdsWithin_mono _ Ico_subset_Icc_self)
[GOAL]
case mk.inl.intro.left.refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : LinearOrderedRing α
inst✝⁴ : FloorRing α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : β → α → γ
h : ContinuousOn (uncurry f) (univ ×ˢ Icc 0 1)
hf : ∀ (s : β), f s 0 = f s 1
s : β
n : ℤ
⊢ 𝓝 (uncurry f (s, 1)) = 𝓝 ((uncurry f ∘ Prod.map id fract) (s, ↑n))
[PROOFSTEP]
simp [hf]
[GOAL]
case mk.inl.intro.right
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : LinearOrderedRing α
inst✝⁴ : FloorRing α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : β → α → γ
h : ContinuousOn (uncurry f) (univ ×ˢ Icc 0 1)
hf : ∀ (s : β), f s 0 = f s 1
s : β
n : ℤ
⊢ Tendsto (uncurry f ∘ Prod.map id fract) (𝓝 s ×ˢ 𝓝[Ici ↑n] ↑n) (𝓝 ((uncurry f ∘ Prod.map id fract) (s, ↑n)))
[PROOFSTEP]
refine
  (((h (s, 0) ⟨trivial, le_rfl, zero_le_one⟩).tendsto.mono_left <| le_of_eq ?_).comp
        (tendsto_id.prod_map (tendsto_fract_right _))).mono_right
    (le_of_eq ?_)
[GOAL]
case mk.inl.intro.right.refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : LinearOrderedRing α
inst✝⁴ : FloorRing α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : β → α → γ
h : ContinuousOn (uncurry f) (univ ×ˢ Icc 0 1)
hf : ∀ (s : β), f s 0 = f s 1
s : β
n : ℤ
⊢ 𝓝 s ×ˢ 𝓝[Ici 0] 0 = 𝓝[univ ×ˢ Icc 0 1] (s, 0)
[PROOFSTEP]
simp [nhdsWithin_prod_eq, nhdsWithin_univ]
[GOAL]
case mk.inl.intro.right.refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : LinearOrderedRing α
inst✝⁴ : FloorRing α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : β → α → γ
h : ContinuousOn (uncurry f) (univ ×ˢ Icc 0 1)
hf : ∀ (s : β), f s 0 = f s 1
s : β
n : ℤ
⊢ 𝓝 (uncurry f (s, 0)) = 𝓝 ((uncurry f ∘ Prod.map id fract) (s, ↑n))
[PROOFSTEP]
simp [nhdsWithin_prod_eq, nhdsWithin_univ]
[GOAL]
case mk.inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : LinearOrderedRing α
inst✝⁴ : FloorRing α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : β → α → γ
h : ContinuousOn (uncurry f) (univ ×ˢ Icc 0 1)
hf : ∀ (s : β), f s 0 = f s 1
s : β
t : α
ht : ¬∃ n, t = ↑n
⊢ ContinuousAt (uncurry f ∘ Prod.map id fract) (s, t)
[PROOFSTEP]
replace ht : t ≠ ⌊t⌋ := fun ht' => ht ⟨_, ht'⟩
[GOAL]
case mk.inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : LinearOrderedRing α
inst✝⁴ : FloorRing α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : β → α → γ
h : ContinuousOn (uncurry f) (univ ×ˢ Icc 0 1)
hf : ∀ (s : β), f s 0 = f s 1
s : β
t : α
ht : t ≠ ↑⌊t⌋
⊢ ContinuousAt (uncurry f ∘ Prod.map id fract) (s, t)
[PROOFSTEP]
refine (h.continuousAt ?_).comp (continuousAt_id.prod_map (continuousAt_fract ht))
[GOAL]
case mk.inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : LinearOrderedRing α
inst✝⁴ : FloorRing α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : β → α → γ
h : ContinuousOn (uncurry f) (univ ×ˢ Icc 0 1)
hf : ∀ (s : β), f s 0 = f s 1
s : β
t : α
ht : t ≠ ↑⌊t⌋
⊢ univ ×ˢ Icc 0 1 ∈ 𝓝 (Prod.map id fract (s, t))
[PROOFSTEP]
exact prod_mem_nhds univ_mem (Icc_mem_nhds (fract_pos.2 ht) (fract_lt_one _))


[GOAL]
X : Type u
α : Type v
inst✝⁴ : TopologicalSpace X
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderClosedTopology α
inst✝ : PreconnectedSpace X
a b : X
f g : X → α
hf : Continuous f
hg : Continuous g
ha : f a ≤ g a
hb : g b ≤ f b
⊢ ∃ x, f x = g x
[PROOFSTEP]
obtain ⟨x, _, hfg, hgf⟩ : (univ ∩ {x | f x ≤ g x ∧ g x ≤ f x}).Nonempty
[GOAL]
X : Type u
α : Type v
inst✝⁴ : TopologicalSpace X
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderClosedTopology α
inst✝ : PreconnectedSpace X
a b : X
f g : X → α
hf : Continuous f
hg : Continuous g
ha : f a ≤ g a
hb : g b ≤ f b
⊢ Set.Nonempty (univ ∩ {x | f x ≤ g x ∧ g x ≤ f x})
case intro.intro.intro
X : Type u
α : Type v
inst✝⁴ : TopologicalSpace X
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderClosedTopology α
inst✝ : PreconnectedSpace X
a b : X
f g : X → α
hf : Continuous f
hg : Continuous g
ha : f a ≤ g a
hb : g b ≤ f b
x : X
left✝ : x ∈ univ
hfg : f x ≤ g x
hgf : g x ≤ f x
⊢ ∃ x, f x = g x
[PROOFSTEP]
exact
  isPreconnected_closed_iff.1 PreconnectedSpace.isPreconnected_univ _ _ (isClosed_le hf hg) (isClosed_le hg hf)
    (fun _ _ => le_total _ _) ⟨a, trivial, ha⟩ ⟨b, trivial, hb⟩
[GOAL]
case intro.intro.intro
X : Type u
α : Type v
inst✝⁴ : TopologicalSpace X
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderClosedTopology α
inst✝ : PreconnectedSpace X
a b : X
f g : X → α
hf : Continuous f
hg : Continuous g
ha : f a ≤ g a
hb : g b ≤ f b
x : X
left✝ : x ∈ univ
hfg : f x ≤ g x
hgf : g x ≤ f x
⊢ ∃ x, f x = g x
[PROOFSTEP]
exact ⟨x, le_antisymm hfg hgf⟩
[GOAL]
X : Type u
α : Type v
inst✝⁴ : TopologicalSpace X
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderClosedTopology α
s : Set X
hs : IsPreconnected s
a : X
l : Filter X
ha : a ∈ s
inst✝ : NeBot l
hl : l ≤ 𝓟 s
f g : X → α
hf : ContinuousOn f s
hg : ContinuousOn g s
ha' : f a ≤ g a
he : g ≤ᶠ[l] f
⊢ ∃ x, x ∈ s ∧ f x = g x
[PROOFSTEP]
rw [continuousOn_iff_continuous_restrict] at hf hg
[GOAL]
X : Type u
α : Type v
inst✝⁴ : TopologicalSpace X
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderClosedTopology α
s : Set X
hs : IsPreconnected s
a : X
l : Filter X
ha : a ∈ s
inst✝ : NeBot l
hl : l ≤ 𝓟 s
f g : X → α
hf : Continuous (restrict s f)
hg : Continuous (restrict s g)
ha' : f a ≤ g a
he : g ≤ᶠ[l] f
⊢ ∃ x, x ∈ s ∧ f x = g x
[PROOFSTEP]
obtain ⟨b, h⟩ :=
  @intermediate_value_univ₂_eventually₁ _ _ _ _ _ _ (Subtype.preconnectedSpace hs) ⟨a, ha⟩ _
    (comap_coe_neBot_of_le_principal hl) _ _ hf hg ha' (he.comap _)
[GOAL]
case intro
X : Type u
α : Type v
inst✝⁴ : TopologicalSpace X
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderClosedTopology α
s : Set X
hs : IsPreconnected s
a : X
l : Filter X
ha : a ∈ s
inst✝ : NeBot l
hl : l ≤ 𝓟 s
f g : X → α
hf : Continuous (restrict s f)
hg : Continuous (restrict s g)
ha' : f a ≤ g a
he : g ≤ᶠ[l] f
b : ↑s
h : restrict s f b = restrict s g b
⊢ ∃ x, x ∈ s ∧ f x = g x
[PROOFSTEP]
exact ⟨b, b.prop, h⟩
[GOAL]
X : Type u
α : Type v
inst✝⁵ : TopologicalSpace X
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderClosedTopology α
s : Set X
hs : IsPreconnected s
l₁ l₂ : Filter X
inst✝¹ : NeBot l₁
inst✝ : NeBot l₂
hl₁ : l₁ ≤ 𝓟 s
hl₂ : l₂ ≤ 𝓟 s
f g : X → α
hf : ContinuousOn f s
hg : ContinuousOn g s
he₁ : f ≤ᶠ[l₁] g
he₂ : g ≤ᶠ[l₂] f
⊢ ∃ x, x ∈ s ∧ f x = g x
[PROOFSTEP]
rw [continuousOn_iff_continuous_restrict] at hf hg
[GOAL]
X : Type u
α : Type v
inst✝⁵ : TopologicalSpace X
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderClosedTopology α
s : Set X
hs : IsPreconnected s
l₁ l₂ : Filter X
inst✝¹ : NeBot l₁
inst✝ : NeBot l₂
hl₁ : l₁ ≤ 𝓟 s
hl₂ : l₂ ≤ 𝓟 s
f g : X → α
hf : Continuous (restrict s f)
hg : Continuous (restrict s g)
he₁ : f ≤ᶠ[l₁] g
he₂ : g ≤ᶠ[l₂] f
⊢ ∃ x, x ∈ s ∧ f x = g x
[PROOFSTEP]
obtain ⟨b, h⟩ :=
  @intermediate_value_univ₂_eventually₂ _ _ _ _ _ _ (Subtype.preconnectedSpace hs) _ _
    (comap_coe_neBot_of_le_principal hl₁) (comap_coe_neBot_of_le_principal hl₂) _ _ hf hg (he₁.comap _) (he₂.comap _)
[GOAL]
case intro
X : Type u
α : Type v
inst✝⁵ : TopologicalSpace X
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderClosedTopology α
s : Set X
hs : IsPreconnected s
l₁ l₂ : Filter X
inst✝¹ : NeBot l₁
inst✝ : NeBot l₂
hl₁ : l₁ ≤ 𝓟 s
hl₂ : l₂ ≤ 𝓟 s
f g : X → α
hf : Continuous (restrict s f)
hg : Continuous (restrict s g)
he₁ : f ≤ᶠ[l₁] g
he₂ : g ≤ᶠ[l₂] f
b : ↑s
h : restrict s f b = restrict s g b
⊢ ∃ x, x ∈ s ∧ f x = g x
[PROOFSTEP]
exact ⟨b, b.prop, h⟩
[GOAL]
X : Type u
α : Type v
inst✝³ : TopologicalSpace X
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
s : Set α
hs : IsPreconnected s
a b : α
ha : a ∈ s
hb : b ∈ s
⊢ Icc a b ⊆ s
[PROOFSTEP]
simpa only [image_id] using hs.intermediate_value ha hb continuousOn_id
[GOAL]
X : Type u
α : Type v
inst✝³ : TopologicalSpace X
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
s : Set α
hs : IsPreconnected s
hb : ¬BddBelow s
ha : ¬BddAbove s
⊢ s = univ
[PROOFSTEP]
refine' eq_univ_of_forall fun x => _
[GOAL]
X : Type u
α : Type v
inst✝³ : TopologicalSpace X
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
s : Set α
hs : IsPreconnected s
hb : ¬BddBelow s
ha : ¬BddAbove s
x : α
⊢ x ∈ s
[PROOFSTEP]
obtain ⟨y, ys, hy⟩ : ∃ y ∈ s, y < x := not_bddBelow_iff.1 hb x
[GOAL]
case intro.intro
X : Type u
α : Type v
inst✝³ : TopologicalSpace X
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
s : Set α
hs : IsPreconnected s
hb : ¬BddBelow s
ha : ¬BddAbove s
x y : α
ys : y ∈ s
hy : y < x
⊢ x ∈ s
[PROOFSTEP]
obtain ⟨z, zs, hz⟩ : ∃ z ∈ s, x < z := not_bddAbove_iff.1 ha x
[GOAL]
case intro.intro.intro.intro
X : Type u
α : Type v
inst✝³ : TopologicalSpace X
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
s : Set α
hs : IsPreconnected s
hb : ¬BddBelow s
ha : ¬BddAbove s
x y : α
ys : y ∈ s
hy : y < x
z : α
zs : z ∈ s
hz : x < z
⊢ x ∈ s
[PROOFSTEP]
exact hs.Icc_subset ys zs ⟨le_of_lt hy, le_of_lt hz⟩
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
s : Set α
hs : IsPreconnected s
⊢ s ∈
    {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
      Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
[PROOFSTEP]
rcases s.eq_empty_or_nonempty with (rfl | hne)
[GOAL]
case inl
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
hs : IsPreconnected ∅
⊢ ∅ ∈
    {Icc (sInf ∅) (sSup ∅), Ico (sInf ∅) (sSup ∅), Ioc (sInf ∅) (sSup ∅), Ioo (sInf ∅) (sSup ∅), Ici (sInf ∅),
      Ioi (sInf ∅), Iic (sSup ∅), Iio (sSup ∅), univ, ∅}
[PROOFSTEP]
apply_rules [Or.inr, mem_singleton]
[GOAL]
case inr
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
s : Set α
hs : IsPreconnected s
hne : Set.Nonempty s
⊢ s ∈
    {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
      Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
[PROOFSTEP]
have hs' : IsConnected s := ⟨hne, hs⟩
[GOAL]
case inr
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
s : Set α
hs : IsPreconnected s
hne : Set.Nonempty s
hs' : IsConnected s
⊢ s ∈
    {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
      Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
[PROOFSTEP]
by_cases hb : BddBelow s
[GOAL]
case pos
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
s : Set α
hs : IsPreconnected s
hne : Set.Nonempty s
hs' : IsConnected s
hb : BddBelow s
⊢ s ∈
    {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
      Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
[PROOFSTEP]
by_cases ha : BddAbove s
[GOAL]
case neg
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
s : Set α
hs : IsPreconnected s
hne : Set.Nonempty s
hs' : IsConnected s
hb : ¬BddBelow s
⊢ s ∈
    {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
      Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
[PROOFSTEP]
by_cases ha : BddAbove s
[GOAL]
case pos
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
s : Set α
hs : IsPreconnected s
hne : Set.Nonempty s
hs' : IsConnected s
hb : BddBelow s
ha : BddAbove s
⊢ s ∈
    {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
      Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
[PROOFSTEP]
rcases mem_Icc_Ico_Ioc_Ioo_of_subset_of_subset (hs'.Ioo_csInf_csSup_subset hb ha) (subset_Icc_csInf_csSup hb ha) with
  (hs | hs | hs | hs)
[GOAL]
case pos.inl
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
s : Set α
hs✝ : IsPreconnected s
hne : Set.Nonempty s
hs' : IsConnected s
hb : BddBelow s
ha : BddAbove s
hs : s = Icc (sInf s) (sSup s)
⊢ s ∈
    {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
      Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
[PROOFSTEP]
exact Or.inl hs
[GOAL]
case pos.inr.inl
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
s : Set α
hs✝ : IsPreconnected s
hne : Set.Nonempty s
hs' : IsConnected s
hb : BddBelow s
ha : BddAbove s
hs : s = Ico (sInf s) (sSup s)
⊢ s ∈
    {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
      Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
[PROOFSTEP]
exact Or.inr <| Or.inl hs
[GOAL]
case pos.inr.inr.inl
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
s : Set α
hs✝ : IsPreconnected s
hne : Set.Nonempty s
hs' : IsConnected s
hb : BddBelow s
ha : BddAbove s
hs : s = Ioc (sInf s) (sSup s)
⊢ s ∈
    {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
      Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
[PROOFSTEP]
exact Or.inr <| Or.inr <| Or.inl hs
[GOAL]
case pos.inr.inr.inr
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
s : Set α
hs✝ : IsPreconnected s
hne : Set.Nonempty s
hs' : IsConnected s
hb : BddBelow s
ha : BddAbove s
hs : s ∈ {Ioo (sInf s) (sSup s)}
⊢ s ∈
    {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
      Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
[PROOFSTEP]
exact Or.inr <| Or.inr <| Or.inr <| Or.inl hs
[GOAL]
case neg
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
s : Set α
hs : IsPreconnected s
hne : Set.Nonempty s
hs' : IsConnected s
hb : BddBelow s
ha : ¬BddAbove s
⊢ s ∈
    {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
      Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
[PROOFSTEP]
refine' Or.inr <| Or.inr <| Or.inr <| Or.inr _
[GOAL]
case neg
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
s : Set α
hs : IsPreconnected s
hne : Set.Nonempty s
hs' : IsConnected s
hb : BddBelow s
ha : ¬BddAbove s
⊢ s ∈ {Ici (sInf s), Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
[PROOFSTEP]
cases' mem_Ici_Ioi_of_subset_of_subset (hs.Ioi_csInf_subset hb ha) fun x hx => csInf_le hb hx with hs hs
[GOAL]
case neg.inl
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
s : Set α
hs✝ : IsPreconnected s
hne : Set.Nonempty s
hs' : IsConnected s
hb : BddBelow s
ha : ¬BddAbove s
hs : s = Ici (sInf s)
⊢ s ∈ {Ici (sInf s), Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
[PROOFSTEP]
exact Or.inl hs
[GOAL]
case neg.inr
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
s : Set α
hs✝ : IsPreconnected s
hne : Set.Nonempty s
hs' : IsConnected s
hb : BddBelow s
ha : ¬BddAbove s
hs : s ∈ {Ioi (sInf s)}
⊢ s ∈ {Ici (sInf s), Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
[PROOFSTEP]
exact Or.inr (Or.inl hs)
[GOAL]
case pos
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
s : Set α
hs : IsPreconnected s
hne : Set.Nonempty s
hs' : IsConnected s
hb : ¬BddBelow s
ha : BddAbove s
⊢ s ∈
    {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
      Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
[PROOFSTEP]
iterate 6 apply Or.inr
[GOAL]
case pos
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
s : Set α
hs : IsPreconnected s
hne : Set.Nonempty s
hs' : IsConnected s
hb : ¬BddBelow s
ha : BddAbove s
⊢ s ∈
    {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
      Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
[PROOFSTEP]
apply Or.inr
[GOAL]
case pos.h
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
s : Set α
hs : IsPreconnected s
hne : Set.Nonempty s
hs' : IsConnected s
hb : ¬BddBelow s
ha : BddAbove s
⊢ s ∈
    {Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s), Ioi (sInf s), Iic (sSup s),
      Iio (sSup s), univ, ∅}
[PROOFSTEP]
apply Or.inr
[GOAL]
case pos.h.h
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
s : Set α
hs : IsPreconnected s
hne : Set.Nonempty s
hs' : IsConnected s
hb : ¬BddBelow s
ha : BddAbove s
⊢ s ∈ {Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s), Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
[PROOFSTEP]
apply Or.inr
[GOAL]
case pos.h.h.h
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
s : Set α
hs : IsPreconnected s
hne : Set.Nonempty s
hs' : IsConnected s
hb : ¬BddBelow s
ha : BddAbove s
⊢ s ∈ {Ioo (sInf s) (sSup s), Ici (sInf s), Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
[PROOFSTEP]
apply Or.inr
[GOAL]
case pos.h.h.h.h
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
s : Set α
hs : IsPreconnected s
hne : Set.Nonempty s
hs' : IsConnected s
hb : ¬BddBelow s
ha : BddAbove s
⊢ s ∈ {Ici (sInf s), Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
[PROOFSTEP]
apply Or.inr
[GOAL]
case pos.h.h.h.h.h
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
s : Set α
hs : IsPreconnected s
hne : Set.Nonempty s
hs' : IsConnected s
hb : ¬BddBelow s
ha : BddAbove s
⊢ s ∈ {Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
[PROOFSTEP]
apply Or.inr
[GOAL]
case pos.h.h.h.h.h.h
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
s : Set α
hs : IsPreconnected s
hne : Set.Nonempty s
hs' : IsConnected s
hb : ¬BddBelow s
ha : BddAbove s
⊢ s ∈ {Iic (sSup s), Iio (sSup s), univ, ∅}
[PROOFSTEP]
cases' mem_Iic_Iio_of_subset_of_subset (hs.Iio_csSup_subset hb ha) fun x hx => le_csSup ha hx with hs hs
[GOAL]
case pos.h.h.h.h.h.h.inl
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
s : Set α
hs✝ : IsPreconnected s
hne : Set.Nonempty s
hs' : IsConnected s
hb : ¬BddBelow s
ha : BddAbove s
hs : s = Iic (sSup s)
⊢ s ∈ {Iic (sSup s), Iio (sSup s), univ, ∅}
[PROOFSTEP]
exact Or.inl hs
[GOAL]
case pos.h.h.h.h.h.h.inr
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
s : Set α
hs✝ : IsPreconnected s
hne : Set.Nonempty s
hs' : IsConnected s
hb : ¬BddBelow s
ha : BddAbove s
hs : s ∈ {Iio (sSup s)}
⊢ s ∈ {Iic (sSup s), Iio (sSup s), univ, ∅}
[PROOFSTEP]
exact Or.inr (Or.inl hs)
[GOAL]
case neg
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
s : Set α
hs : IsPreconnected s
hne : Set.Nonempty s
hs' : IsConnected s
hb : ¬BddBelow s
ha : ¬BddAbove s
⊢ s ∈
    {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
      Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
[PROOFSTEP]
iterate 8 apply Or.inr
[GOAL]
case neg
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
s : Set α
hs : IsPreconnected s
hne : Set.Nonempty s
hs' : IsConnected s
hb : ¬BddBelow s
ha : ¬BddAbove s
⊢ s ∈
    {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
      Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
[PROOFSTEP]
apply Or.inr
[GOAL]
case neg.h
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
s : Set α
hs : IsPreconnected s
hne : Set.Nonempty s
hs' : IsConnected s
hb : ¬BddBelow s
ha : ¬BddAbove s
⊢ s ∈
    {Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s), Ioi (sInf s), Iic (sSup s),
      Iio (sSup s), univ, ∅}
[PROOFSTEP]
apply Or.inr
[GOAL]
case neg.h.h
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
s : Set α
hs : IsPreconnected s
hne : Set.Nonempty s
hs' : IsConnected s
hb : ¬BddBelow s
ha : ¬BddAbove s
⊢ s ∈ {Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s), Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
[PROOFSTEP]
apply Or.inr
[GOAL]
case neg.h.h.h
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
s : Set α
hs : IsPreconnected s
hne : Set.Nonempty s
hs' : IsConnected s
hb : ¬BddBelow s
ha : ¬BddAbove s
⊢ s ∈ {Ioo (sInf s) (sSup s), Ici (sInf s), Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
[PROOFSTEP]
apply Or.inr
[GOAL]
case neg.h.h.h.h
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
s : Set α
hs : IsPreconnected s
hne : Set.Nonempty s
hs' : IsConnected s
hb : ¬BddBelow s
ha : ¬BddAbove s
⊢ s ∈ {Ici (sInf s), Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
[PROOFSTEP]
apply Or.inr
[GOAL]
case neg.h.h.h.h.h
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
s : Set α
hs : IsPreconnected s
hne : Set.Nonempty s
hs' : IsConnected s
hb : ¬BddBelow s
ha : ¬BddAbove s
⊢ s ∈ {Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
[PROOFSTEP]
apply Or.inr
[GOAL]
case neg.h.h.h.h.h.h
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
s : Set α
hs : IsPreconnected s
hne : Set.Nonempty s
hs' : IsConnected s
hb : ¬BddBelow s
ha : ¬BddAbove s
⊢ s ∈ {Iic (sSup s), Iio (sSup s), univ, ∅}
[PROOFSTEP]
apply Or.inr
[GOAL]
case neg.h.h.h.h.h.h.h
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
s : Set α
hs : IsPreconnected s
hne : Set.Nonempty s
hs' : IsConnected s
hb : ¬BddBelow s
ha : ¬BddAbove s
⊢ s ∈ {Iio (sSup s), univ, ∅}
[PROOFSTEP]
apply Or.inr
[GOAL]
case neg.h.h.h.h.h.h.h.h
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
s : Set α
hs : IsPreconnected s
hne : Set.Nonempty s
hs' : IsConnected s
hb : ¬BddBelow s
ha : ¬BddAbove s
⊢ s ∈ {univ, ∅}
[PROOFSTEP]
exact Or.inl (hs.eq_univ_of_unbounded hb ha)
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
⊢ {s | IsPreconnected s} ⊆
    range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅})
[PROOFSTEP]
intro s hs
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
s : Set α
hs : s ∈ {s | IsPreconnected s}
⊢ s ∈
    range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅})
[PROOFSTEP]
rcases hs.mem_intervals with (hs | hs | hs | hs | hs | hs | hs | hs | hs | hs)
[GOAL]
case inl
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
s : Set α
hs✝ : s ∈ {s | IsPreconnected s}
hs : s = Icc (sInf s) (sSup s)
⊢ s ∈
    range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅})
[PROOFSTEP]
exact Or.inl <| Or.inl <| Or.inl <| Or.inl ⟨(sInf s, sSup s), hs.symm⟩
[GOAL]
case inr.inl
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
s : Set α
hs✝ : s ∈ {s | IsPreconnected s}
hs : s = Ico (sInf s) (sSup s)
⊢ s ∈
    range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅})
[PROOFSTEP]
exact Or.inl <| Or.inl <| Or.inl <| Or.inr ⟨(sInf s, sSup s), hs.symm⟩
[GOAL]
case inr.inr.inl
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
s : Set α
hs✝ : s ∈ {s | IsPreconnected s}
hs : s = Ioc (sInf s) (sSup s)
⊢ s ∈
    range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅})
[PROOFSTEP]
exact Or.inl <| Or.inl <| Or.inr ⟨(sInf s, sSup s), hs.symm⟩
[GOAL]
case inr.inr.inr.inl
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
s : Set α
hs✝ : s ∈ {s | IsPreconnected s}
hs : s = Ioo (sInf s) (sSup s)
⊢ s ∈
    range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅})
[PROOFSTEP]
exact Or.inl <| Or.inr ⟨(sInf s, sSup s), hs.symm⟩
[GOAL]
case inr.inr.inr.inr.inl
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
s : Set α
hs✝ : s ∈ {s | IsPreconnected s}
hs : s = Ici (sInf s)
⊢ s ∈
    range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅})
[PROOFSTEP]
exact Or.inr <| Or.inl <| Or.inl <| Or.inl <| Or.inl ⟨sInf s, hs.symm⟩
[GOAL]
case inr.inr.inr.inr.inr.inl
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
s : Set α
hs✝ : s ∈ {s | IsPreconnected s}
hs : s = Ioi (sInf s)
⊢ s ∈
    range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅})
[PROOFSTEP]
exact Or.inr <| Or.inl <| Or.inl <| Or.inl <| Or.inr ⟨sInf s, hs.symm⟩
[GOAL]
case inr.inr.inr.inr.inr.inr.inl
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
s : Set α
hs✝ : s ∈ {s | IsPreconnected s}
hs : s = Iic (sSup s)
⊢ s ∈
    range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅})
[PROOFSTEP]
exact Or.inr <| Or.inl <| Or.inl <| Or.inr ⟨sSup s, hs.symm⟩
[GOAL]
case inr.inr.inr.inr.inr.inr.inr.inl
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
s : Set α
hs✝ : s ∈ {s | IsPreconnected s}
hs : s = Iio (sSup s)
⊢ s ∈
    range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅})
[PROOFSTEP]
exact Or.inr <| Or.inl <| Or.inr ⟨sSup s, hs.symm⟩
[GOAL]
case inr.inr.inr.inr.inr.inr.inr.inr.inl
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
s : Set α
hs✝ : s ∈ {s | IsPreconnected s}
hs : s = univ
⊢ s ∈
    range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅})
[PROOFSTEP]
exact Or.inr <| Or.inr <| Or.inl hs
[GOAL]
case inr.inr.inr.inr.inr.inr.inr.inr.inr
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
s : Set α
hs✝ : s ∈ {s | IsPreconnected s}
hs : s ∈ {∅}
⊢ s ∈
    range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅})
[PROOFSTEP]
exact Or.inr <| Or.inr <| Or.inr hs
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
a b : α
s : Set α
hs : IsClosed (s ∩ Icc a b)
ha : a ∈ s
hab : a ≤ b
hgt : ∀ (x : α), x ∈ s ∩ Ico a b → Set.Nonempty (s ∩ Ioc x b)
⊢ b ∈ s
[PROOFSTEP]
let S := s ∩ Icc a b
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
a b : α
s : Set α
hs : IsClosed (s ∩ Icc a b)
ha : a ∈ s
hab : a ≤ b
hgt : ∀ (x : α), x ∈ s ∩ Ico a b → Set.Nonempty (s ∩ Ioc x b)
S : Set α := s ∩ Icc a b
⊢ b ∈ s
[PROOFSTEP]
replace ha : a ∈ S
[GOAL]
case ha
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
a b : α
s : Set α
hs : IsClosed (s ∩ Icc a b)
ha : a ∈ s
hab : a ≤ b
hgt : ∀ (x : α), x ∈ s ∩ Ico a b → Set.Nonempty (s ∩ Ioc x b)
S : Set α := s ∩ Icc a b
⊢ a ∈ S
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
a b : α
s : Set α
hs : IsClosed (s ∩ Icc a b)
hab : a ≤ b
hgt : ∀ (x : α), x ∈ s ∩ Ico a b → Set.Nonempty (s ∩ Ioc x b)
S : Set α := s ∩ Icc a b
ha : a ∈ S
⊢ b ∈ s
[PROOFSTEP]
exact ⟨ha, left_mem_Icc.2 hab⟩
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
a b : α
s : Set α
hs : IsClosed (s ∩ Icc a b)
hab : a ≤ b
hgt : ∀ (x : α), x ∈ s ∩ Ico a b → Set.Nonempty (s ∩ Ioc x b)
S : Set α := s ∩ Icc a b
ha : a ∈ S
⊢ b ∈ s
[PROOFSTEP]
have Sbd : BddAbove S := ⟨b, fun z hz => hz.2.2⟩
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
a b : α
s : Set α
hs : IsClosed (s ∩ Icc a b)
hab : a ≤ b
hgt : ∀ (x : α), x ∈ s ∩ Ico a b → Set.Nonempty (s ∩ Ioc x b)
S : Set α := s ∩ Icc a b
ha : a ∈ S
Sbd : BddAbove S
⊢ b ∈ s
[PROOFSTEP]
let c := sSup (s ∩ Icc a b)
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
a b : α
s : Set α
hs : IsClosed (s ∩ Icc a b)
hab : a ≤ b
hgt : ∀ (x : α), x ∈ s ∩ Ico a b → Set.Nonempty (s ∩ Ioc x b)
S : Set α := s ∩ Icc a b
ha : a ∈ S
Sbd : BddAbove S
c : α := sSup (s ∩ Icc a b)
⊢ b ∈ s
[PROOFSTEP]
have c_mem : c ∈ S := hs.csSup_mem ⟨_, ha⟩ Sbd
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
a b : α
s : Set α
hs : IsClosed (s ∩ Icc a b)
hab : a ≤ b
hgt : ∀ (x : α), x ∈ s ∩ Ico a b → Set.Nonempty (s ∩ Ioc x b)
S : Set α := s ∩ Icc a b
ha : a ∈ S
Sbd : BddAbove S
c : α := sSup (s ∩ Icc a b)
c_mem : c ∈ S
⊢ b ∈ s
[PROOFSTEP]
have c_le : c ≤ b := csSup_le ⟨_, ha⟩ fun x hx => hx.2.2
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
a b : α
s : Set α
hs : IsClosed (s ∩ Icc a b)
hab : a ≤ b
hgt : ∀ (x : α), x ∈ s ∩ Ico a b → Set.Nonempty (s ∩ Ioc x b)
S : Set α := s ∩ Icc a b
ha : a ∈ S
Sbd : BddAbove S
c : α := sSup (s ∩ Icc a b)
c_mem : c ∈ S
c_le : c ≤ b
⊢ b ∈ s
[PROOFSTEP]
cases' eq_or_lt_of_le c_le with hc hc
[GOAL]
case inl
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
a b : α
s : Set α
hs : IsClosed (s ∩ Icc a b)
hab : a ≤ b
hgt : ∀ (x : α), x ∈ s ∩ Ico a b → Set.Nonempty (s ∩ Ioc x b)
S : Set α := s ∩ Icc a b
ha : a ∈ S
Sbd : BddAbove S
c : α := sSup (s ∩ Icc a b)
c_mem : c ∈ S
c_le : c ≤ b
hc : c = b
⊢ b ∈ s
case inr
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
a b : α
s : Set α
hs : IsClosed (s ∩ Icc a b)
hab : a ≤ b
hgt : ∀ (x : α), x ∈ s ∩ Ico a b → Set.Nonempty (s ∩ Ioc x b)
S : Set α := s ∩ Icc a b
ha : a ∈ S
Sbd : BddAbove S
c : α := sSup (s ∩ Icc a b)
c_mem : c ∈ S
c_le : c ≤ b
hc : c < b
⊢ b ∈ s
[PROOFSTEP]
exact hc ▸ c_mem.1
[GOAL]
case inr
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
a b : α
s : Set α
hs : IsClosed (s ∩ Icc a b)
hab : a ≤ b
hgt : ∀ (x : α), x ∈ s ∩ Ico a b → Set.Nonempty (s ∩ Ioc x b)
S : Set α := s ∩ Icc a b
ha : a ∈ S
Sbd : BddAbove S
c : α := sSup (s ∩ Icc a b)
c_mem : c ∈ S
c_le : c ≤ b
hc : c < b
⊢ b ∈ s
[PROOFSTEP]
exfalso
[GOAL]
case inr.h
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
a b : α
s : Set α
hs : IsClosed (s ∩ Icc a b)
hab : a ≤ b
hgt : ∀ (x : α), x ∈ s ∩ Ico a b → Set.Nonempty (s ∩ Ioc x b)
S : Set α := s ∩ Icc a b
ha : a ∈ S
Sbd : BddAbove S
c : α := sSup (s ∩ Icc a b)
c_mem : c ∈ S
c_le : c ≤ b
hc : c < b
⊢ False
[PROOFSTEP]
rcases hgt c ⟨c_mem.1, c_mem.2.1, hc⟩ with ⟨x, xs, cx, xb⟩
[GOAL]
case inr.h.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
a b : α
s : Set α
hs : IsClosed (s ∩ Icc a b)
hab : a ≤ b
hgt : ∀ (x : α), x ∈ s ∩ Ico a b → Set.Nonempty (s ∩ Ioc x b)
S : Set α := s ∩ Icc a b
ha : a ∈ S
Sbd : BddAbove S
c : α := sSup (s ∩ Icc a b)
c_mem : c ∈ S
c_le : c ≤ b
hc : c < b
x : α
xs : x ∈ s
cx : c < x
xb : x ≤ b
⊢ False
[PROOFSTEP]
exact not_lt_of_le (le_csSup Sbd ⟨xs, le_trans (le_csSup Sbd ha) (le_of_lt cx), xb⟩) cx
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
a b : α
s : Set α
hs : IsClosed (s ∩ Icc a b)
ha : a ∈ s
hgt : ∀ (x : α), x ∈ s ∩ Ico a b → ∀ (y : α), y ∈ Ioi x → Set.Nonempty (s ∩ Ioc x y)
⊢ Icc a b ⊆ s
[PROOFSTEP]
intro y hy
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
a b : α
s : Set α
hs : IsClosed (s ∩ Icc a b)
ha : a ∈ s
hgt : ∀ (x : α), x ∈ s ∩ Ico a b → ∀ (y : α), y ∈ Ioi x → Set.Nonempty (s ∩ Ioc x y)
y : α
hy : y ∈ Icc a b
⊢ y ∈ s
[PROOFSTEP]
have : IsClosed (s ∩ Icc a y) :=
  by
  suffices s ∩ Icc a y = s ∩ Icc a b ∩ Icc a y by
    rw [this]
    exact IsClosed.inter hs isClosed_Icc
  rw [inter_assoc]
  congr
  exact (inter_eq_self_of_subset_right <| Icc_subset_Icc_right hy.2).symm
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
a b : α
s : Set α
hs : IsClosed (s ∩ Icc a b)
ha : a ∈ s
hgt : ∀ (x : α), x ∈ s ∩ Ico a b → ∀ (y : α), y ∈ Ioi x → Set.Nonempty (s ∩ Ioc x y)
y : α
hy : y ∈ Icc a b
⊢ IsClosed (s ∩ Icc a y)
[PROOFSTEP]
suffices s ∩ Icc a y = s ∩ Icc a b ∩ Icc a y by
  rw [this]
  exact IsClosed.inter hs isClosed_Icc
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
a b : α
s : Set α
hs : IsClosed (s ∩ Icc a b)
ha : a ∈ s
hgt : ∀ (x : α), x ∈ s ∩ Ico a b → ∀ (y : α), y ∈ Ioi x → Set.Nonempty (s ∩ Ioc x y)
y : α
hy : y ∈ Icc a b
this : s ∩ Icc a y = s ∩ Icc a b ∩ Icc a y
⊢ IsClosed (s ∩ Icc a y)
[PROOFSTEP]
rw [this]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
a b : α
s : Set α
hs : IsClosed (s ∩ Icc a b)
ha : a ∈ s
hgt : ∀ (x : α), x ∈ s ∩ Ico a b → ∀ (y : α), y ∈ Ioi x → Set.Nonempty (s ∩ Ioc x y)
y : α
hy : y ∈ Icc a b
this : s ∩ Icc a y = s ∩ Icc a b ∩ Icc a y
⊢ IsClosed (s ∩ Icc a b ∩ Icc a y)
[PROOFSTEP]
exact IsClosed.inter hs isClosed_Icc
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
a b : α
s : Set α
hs : IsClosed (s ∩ Icc a b)
ha : a ∈ s
hgt : ∀ (x : α), x ∈ s ∩ Ico a b → ∀ (y : α), y ∈ Ioi x → Set.Nonempty (s ∩ Ioc x y)
y : α
hy : y ∈ Icc a b
⊢ s ∩ Icc a y = s ∩ Icc a b ∩ Icc a y
[PROOFSTEP]
rw [inter_assoc]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
a b : α
s : Set α
hs : IsClosed (s ∩ Icc a b)
ha : a ∈ s
hgt : ∀ (x : α), x ∈ s ∩ Ico a b → ∀ (y : α), y ∈ Ioi x → Set.Nonempty (s ∩ Ioc x y)
y : α
hy : y ∈ Icc a b
⊢ s ∩ Icc a y = s ∩ (Icc a b ∩ Icc a y)
[PROOFSTEP]
congr
[GOAL]
case e_a
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
a b : α
s : Set α
hs : IsClosed (s ∩ Icc a b)
ha : a ∈ s
hgt : ∀ (x : α), x ∈ s ∩ Ico a b → ∀ (y : α), y ∈ Ioi x → Set.Nonempty (s ∩ Ioc x y)
y : α
hy : y ∈ Icc a b
⊢ Icc a y = Icc a b ∩ Icc a y
[PROOFSTEP]
exact (inter_eq_self_of_subset_right <| Icc_subset_Icc_right hy.2).symm
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
a b : α
s : Set α
hs : IsClosed (s ∩ Icc a b)
ha : a ∈ s
hgt : ∀ (x : α), x ∈ s ∩ Ico a b → ∀ (y : α), y ∈ Ioi x → Set.Nonempty (s ∩ Ioc x y)
y : α
hy : y ∈ Icc a b
this : IsClosed (s ∩ Icc a y)
⊢ y ∈ s
[PROOFSTEP]
exact
  IsClosed.mem_of_ge_of_forall_exists_gt this ha hy.1 fun x hx => hgt x ⟨hx.1, Ico_subset_Ico_right hy.2 hx.2⟩ y hx.2.2
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝⁷ : ConditionallyCompleteLinearOrder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
inst✝¹ : Nonempty γ
inst✝ : DenselyOrdered α
a✝ b✝ a b : α
s : Set α
hs : IsClosed (s ∩ Icc a b)
ha : a ∈ s
hgt : ∀ (x : α), x ∈ s ∩ Ico a b → s ∈ 𝓝[Ioi x] x
⊢ Icc a b ⊆ s
[PROOFSTEP]
apply hs.Icc_subset_of_forall_exists_gt ha
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝⁷ : ConditionallyCompleteLinearOrder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
inst✝¹ : Nonempty γ
inst✝ : DenselyOrdered α
a✝ b✝ a b : α
s : Set α
hs : IsClosed (s ∩ Icc a b)
ha : a ∈ s
hgt : ∀ (x : α), x ∈ s ∩ Ico a b → s ∈ 𝓝[Ioi x] x
⊢ ∀ (x : α), x ∈ s ∩ Ico a b → ∀ (y : α), y ∈ Ioi x → Set.Nonempty (s ∩ Ioc x y)
[PROOFSTEP]
rintro x ⟨hxs, hxab⟩ y hyxb
[GOAL]
case intro
α : Type u
β : Type v
γ : Type w
inst✝⁷ : ConditionallyCompleteLinearOrder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
inst✝¹ : Nonempty γ
inst✝ : DenselyOrdered α
a✝ b✝ a b : α
s : Set α
hs : IsClosed (s ∩ Icc a b)
ha : a ∈ s
hgt : ∀ (x : α), x ∈ s ∩ Ico a b → s ∈ 𝓝[Ioi x] x
x : α
hxs : x ∈ s
hxab : x ∈ Ico a b
y : α
hyxb : y ∈ Ioi x
⊢ Set.Nonempty (s ∩ Ioc x y)
[PROOFSTEP]
have : s ∩ Ioc x y ∈ 𝓝[>] x := inter_mem (hgt x ⟨hxs, hxab⟩) (Ioc_mem_nhdsWithin_Ioi ⟨le_rfl, hyxb⟩)
[GOAL]
case intro
α : Type u
β : Type v
γ : Type w
inst✝⁷ : ConditionallyCompleteLinearOrder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
inst✝¹ : Nonempty γ
inst✝ : DenselyOrdered α
a✝ b✝ a b : α
s : Set α
hs : IsClosed (s ∩ Icc a b)
ha : a ∈ s
hgt : ∀ (x : α), x ∈ s ∩ Ico a b → s ∈ 𝓝[Ioi x] x
x : α
hxs : x ∈ s
hxab : x ∈ Ico a b
y : α
hyxb : y ∈ Ioi x
this : s ∩ Ioc x y ∈ 𝓝[Ioi x] x
⊢ Set.Nonempty (s ∩ Ioc x y)
[PROOFSTEP]
exact (nhdsWithin_Ioi_self_neBot' ⟨b, hxab.2⟩).nonempty_of_mem this
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝⁷ : ConditionallyCompleteLinearOrder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
inst✝¹ : Nonempty γ
inst✝ : DenselyOrdered α
a b x y : α
s t : Set α
hxy : x ≤ y
hs : IsClosed s
ht : IsClosed t
hab : Icc a b ⊆ s ∪ t
hx : x ∈ Icc a b ∩ s
hy : y ∈ Icc a b ∩ t
⊢ Set.Nonempty (Icc a b ∩ (s ∩ t))
[PROOFSTEP]
have xyab : Icc x y ⊆ Icc a b := Icc_subset_Icc hx.1.1 hy.1.2
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝⁷ : ConditionallyCompleteLinearOrder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
inst✝¹ : Nonempty γ
inst✝ : DenselyOrdered α
a b x y : α
s t : Set α
hxy : x ≤ y
hs : IsClosed s
ht : IsClosed t
hab : Icc a b ⊆ s ∪ t
hx : x ∈ Icc a b ∩ s
hy : y ∈ Icc a b ∩ t
xyab : Icc x y ⊆ Icc a b
⊢ Set.Nonempty (Icc a b ∩ (s ∩ t))
[PROOFSTEP]
by_contra hst
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝⁷ : ConditionallyCompleteLinearOrder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
inst✝¹ : Nonempty γ
inst✝ : DenselyOrdered α
a b x y : α
s t : Set α
hxy : x ≤ y
hs : IsClosed s
ht : IsClosed t
hab : Icc a b ⊆ s ∪ t
hx : x ∈ Icc a b ∩ s
hy : y ∈ Icc a b ∩ t
xyab : Icc x y ⊆ Icc a b
hst : ¬Set.Nonempty (Icc a b ∩ (s ∩ t))
⊢ False
[PROOFSTEP]
suffices : Icc x y ⊆ s
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝⁷ : ConditionallyCompleteLinearOrder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
inst✝¹ : Nonempty γ
inst✝ : DenselyOrdered α
a b x y : α
s t : Set α
hxy : x ≤ y
hs : IsClosed s
ht : IsClosed t
hab : Icc a b ⊆ s ∪ t
hx : x ∈ Icc a b ∩ s
hy : y ∈ Icc a b ∩ t
xyab : Icc x y ⊆ Icc a b
hst : ¬Set.Nonempty (Icc a b ∩ (s ∩ t))
this : Icc x y ⊆ s
⊢ False
case this
α : Type u
β : Type v
γ : Type w
inst✝⁷ : ConditionallyCompleteLinearOrder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
inst✝¹ : Nonempty γ
inst✝ : DenselyOrdered α
a b x y : α
s t : Set α
hxy : x ≤ y
hs : IsClosed s
ht : IsClosed t
hab : Icc a b ⊆ s ∪ t
hx : x ∈ Icc a b ∩ s
hy : y ∈ Icc a b ∩ t
xyab : Icc x y ⊆ Icc a b
hst : ¬Set.Nonempty (Icc a b ∩ (s ∩ t))
⊢ Icc x y ⊆ s
[PROOFSTEP]
exact hst ⟨y, xyab <| right_mem_Icc.2 hxy, this <| right_mem_Icc.2 hxy, hy.2⟩
[GOAL]
case this
α : Type u
β : Type v
γ : Type w
inst✝⁷ : ConditionallyCompleteLinearOrder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
inst✝¹ : Nonempty γ
inst✝ : DenselyOrdered α
a b x y : α
s t : Set α
hxy : x ≤ y
hs : IsClosed s
ht : IsClosed t
hab : Icc a b ⊆ s ∪ t
hx : x ∈ Icc a b ∩ s
hy : y ∈ Icc a b ∩ t
xyab : Icc x y ⊆ Icc a b
hst : ¬Set.Nonempty (Icc a b ∩ (s ∩ t))
⊢ Icc x y ⊆ s
[PROOFSTEP]
apply (IsClosed.inter hs isClosed_Icc).Icc_subset_of_forall_mem_nhdsWithin hx.2
[GOAL]
case this
α : Type u
β : Type v
γ : Type w
inst✝⁷ : ConditionallyCompleteLinearOrder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
inst✝¹ : Nonempty γ
inst✝ : DenselyOrdered α
a b x y : α
s t : Set α
hxy : x ≤ y
hs : IsClosed s
ht : IsClosed t
hab : Icc a b ⊆ s ∪ t
hx : x ∈ Icc a b ∩ s
hy : y ∈ Icc a b ∩ t
xyab : Icc x y ⊆ Icc a b
hst : ¬Set.Nonempty (Icc a b ∩ (s ∩ t))
⊢ ∀ (x_1 : α), x_1 ∈ s ∩ Ico x y → s ∈ 𝓝[Ioi x_1] x_1
[PROOFSTEP]
rintro z ⟨zs, hz⟩
[GOAL]
case this.intro
α : Type u
β : Type v
γ : Type w
inst✝⁷ : ConditionallyCompleteLinearOrder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
inst✝¹ : Nonempty γ
inst✝ : DenselyOrdered α
a b x y : α
s t : Set α
hxy : x ≤ y
hs : IsClosed s
ht : IsClosed t
hab : Icc a b ⊆ s ∪ t
hx : x ∈ Icc a b ∩ s
hy : y ∈ Icc a b ∩ t
xyab : Icc x y ⊆ Icc a b
hst : ¬Set.Nonempty (Icc a b ∩ (s ∩ t))
z : α
zs : z ∈ s
hz : z ∈ Ico x y
⊢ s ∈ 𝓝[Ioi z] z
[PROOFSTEP]
have zt : z ∈ tᶜ := fun zt => hst ⟨z, xyab <| Ico_subset_Icc_self hz, zs, zt⟩
[GOAL]
case this.intro
α : Type u
β : Type v
γ : Type w
inst✝⁷ : ConditionallyCompleteLinearOrder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
inst✝¹ : Nonempty γ
inst✝ : DenselyOrdered α
a b x y : α
s t : Set α
hxy : x ≤ y
hs : IsClosed s
ht : IsClosed t
hab : Icc a b ⊆ s ∪ t
hx : x ∈ Icc a b ∩ s
hy : y ∈ Icc a b ∩ t
xyab : Icc x y ⊆ Icc a b
hst : ¬Set.Nonempty (Icc a b ∩ (s ∩ t))
z : α
zs : z ∈ s
hz : z ∈ Ico x y
zt : z ∈ tᶜ
⊢ s ∈ 𝓝[Ioi z] z
[PROOFSTEP]
have : tᶜ ∩ Ioc z y ∈ 𝓝[>] z := by
  rw [← nhdsWithin_Ioc_eq_nhdsWithin_Ioi hz.2]
  exact mem_nhdsWithin.2 ⟨tᶜ, ht.isOpen_compl, zt, Subset.rfl⟩
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝⁷ : ConditionallyCompleteLinearOrder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
inst✝¹ : Nonempty γ
inst✝ : DenselyOrdered α
a b x y : α
s t : Set α
hxy : x ≤ y
hs : IsClosed s
ht : IsClosed t
hab : Icc a b ⊆ s ∪ t
hx : x ∈ Icc a b ∩ s
hy : y ∈ Icc a b ∩ t
xyab : Icc x y ⊆ Icc a b
hst : ¬Set.Nonempty (Icc a b ∩ (s ∩ t))
z : α
zs : z ∈ s
hz : z ∈ Ico x y
zt : z ∈ tᶜ
⊢ tᶜ ∩ Ioc z y ∈ 𝓝[Ioi z] z
[PROOFSTEP]
rw [← nhdsWithin_Ioc_eq_nhdsWithin_Ioi hz.2]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝⁷ : ConditionallyCompleteLinearOrder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
inst✝¹ : Nonempty γ
inst✝ : DenselyOrdered α
a b x y : α
s t : Set α
hxy : x ≤ y
hs : IsClosed s
ht : IsClosed t
hab : Icc a b ⊆ s ∪ t
hx : x ∈ Icc a b ∩ s
hy : y ∈ Icc a b ∩ t
xyab : Icc x y ⊆ Icc a b
hst : ¬Set.Nonempty (Icc a b ∩ (s ∩ t))
z : α
zs : z ∈ s
hz : z ∈ Ico x y
zt : z ∈ tᶜ
⊢ tᶜ ∩ Ioc z y ∈ 𝓝[Ioc z y] z
[PROOFSTEP]
exact mem_nhdsWithin.2 ⟨tᶜ, ht.isOpen_compl, zt, Subset.rfl⟩
[GOAL]
case this.intro
α : Type u
β : Type v
γ : Type w
inst✝⁷ : ConditionallyCompleteLinearOrder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
inst✝¹ : Nonempty γ
inst✝ : DenselyOrdered α
a b x y : α
s t : Set α
hxy : x ≤ y
hs : IsClosed s
ht : IsClosed t
hab : Icc a b ⊆ s ∪ t
hx : x ∈ Icc a b ∩ s
hy : y ∈ Icc a b ∩ t
xyab : Icc x y ⊆ Icc a b
hst : ¬Set.Nonempty (Icc a b ∩ (s ∩ t))
z : α
zs : z ∈ s
hz : z ∈ Ico x y
zt : z ∈ tᶜ
this : tᶜ ∩ Ioc z y ∈ 𝓝[Ioi z] z
⊢ s ∈ 𝓝[Ioi z] z
[PROOFSTEP]
apply mem_of_superset this
[GOAL]
case this.intro
α : Type u
β : Type v
γ : Type w
inst✝⁷ : ConditionallyCompleteLinearOrder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
inst✝¹ : Nonempty γ
inst✝ : DenselyOrdered α
a b x y : α
s t : Set α
hxy : x ≤ y
hs : IsClosed s
ht : IsClosed t
hab : Icc a b ⊆ s ∪ t
hx : x ∈ Icc a b ∩ s
hy : y ∈ Icc a b ∩ t
xyab : Icc x y ⊆ Icc a b
hst : ¬Set.Nonempty (Icc a b ∩ (s ∩ t))
z : α
zs : z ∈ s
hz : z ∈ Ico x y
zt : z ∈ tᶜ
this : tᶜ ∩ Ioc z y ∈ 𝓝[Ioi z] z
⊢ tᶜ ∩ Ioc z y ⊆ s
[PROOFSTEP]
have : Ioc z y ⊆ s ∪ t := fun w hw => hab (xyab ⟨le_trans hz.1 (le_of_lt hw.1), hw.2⟩)
[GOAL]
case this.intro
α : Type u
β : Type v
γ : Type w
inst✝⁷ : ConditionallyCompleteLinearOrder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
inst✝¹ : Nonempty γ
inst✝ : DenselyOrdered α
a b x y : α
s t : Set α
hxy : x ≤ y
hs : IsClosed s
ht : IsClosed t
hab : Icc a b ⊆ s ∪ t
hx : x ∈ Icc a b ∩ s
hy : y ∈ Icc a b ∩ t
xyab : Icc x y ⊆ Icc a b
hst : ¬Set.Nonempty (Icc a b ∩ (s ∩ t))
z : α
zs : z ∈ s
hz : z ∈ Ico x y
zt : z ∈ tᶜ
this✝ : tᶜ ∩ Ioc z y ∈ 𝓝[Ioi z] z
this : Ioc z y ⊆ s ∪ t
⊢ tᶜ ∩ Ioc z y ⊆ s
[PROOFSTEP]
exact fun w ⟨wt, wzy⟩ => (this wzy).elim id fun h => (wt h).elim
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝⁷ : ConditionallyCompleteLinearOrder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
inst✝¹ : Nonempty γ
inst✝ : DenselyOrdered α
a b : α
⊢ ∀ (t t' : Set α),
    IsClosed t →
      IsClosed t' →
        Icc a b ⊆ t ∪ t' → Set.Nonempty (Icc a b ∩ t) → Set.Nonempty (Icc a b ∩ t') → Set.Nonempty (Icc a b ∩ (t ∩ t'))
[PROOFSTEP]
rintro s t hs ht hab ⟨x, hx⟩
  ⟨y, hy⟩
      -- This used to use `wlog`, but it was causing timeouts.
[GOAL]
case intro.intro
α : Type u
β : Type v
γ : Type w
inst✝⁷ : ConditionallyCompleteLinearOrder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
inst✝¹ : Nonempty γ
inst✝ : DenselyOrdered α
a b : α
s t : Set α
hs : IsClosed s
ht : IsClosed t
hab : Icc a b ⊆ s ∪ t
x : α
hx : x ∈ Icc a b ∩ s
y : α
hy : y ∈ Icc a b ∩ t
⊢ Set.Nonempty (Icc a b ∩ (s ∩ t))
[PROOFSTEP]
cases' le_total x y with h h
[GOAL]
case intro.intro.inl
α : Type u
β : Type v
γ : Type w
inst✝⁷ : ConditionallyCompleteLinearOrder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
inst✝¹ : Nonempty γ
inst✝ : DenselyOrdered α
a b : α
s t : Set α
hs : IsClosed s
ht : IsClosed t
hab : Icc a b ⊆ s ∪ t
x : α
hx : x ∈ Icc a b ∩ s
y : α
hy : y ∈ Icc a b ∩ t
h : x ≤ y
⊢ Set.Nonempty (Icc a b ∩ (s ∩ t))
[PROOFSTEP]
exact isPreconnected_Icc_aux x y s t h hs ht hab hx hy
[GOAL]
case intro.intro.inr
α : Type u
β : Type v
γ : Type w
inst✝⁷ : ConditionallyCompleteLinearOrder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
inst✝¹ : Nonempty γ
inst✝ : DenselyOrdered α
a b : α
s t : Set α
hs : IsClosed s
ht : IsClosed t
hab : Icc a b ⊆ s ∪ t
x : α
hx : x ∈ Icc a b ∩ s
y : α
hy : y ∈ Icc a b ∩ t
h : y ≤ x
⊢ Set.Nonempty (Icc a b ∩ (s ∩ t))
[PROOFSTEP]
rw [inter_comm s t]
[GOAL]
case intro.intro.inr
α : Type u
β : Type v
γ : Type w
inst✝⁷ : ConditionallyCompleteLinearOrder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
inst✝¹ : Nonempty γ
inst✝ : DenselyOrdered α
a b : α
s t : Set α
hs : IsClosed s
ht : IsClosed t
hab : Icc a b ⊆ s ∪ t
x : α
hx : x ∈ Icc a b ∩ s
y : α
hy : y ∈ Icc a b ∩ t
h : y ≤ x
⊢ Set.Nonempty (Icc a b ∩ (t ∩ s))
[PROOFSTEP]
rw [union_comm s t] at hab
[GOAL]
case intro.intro.inr
α : Type u
β : Type v
γ : Type w
inst✝⁷ : ConditionallyCompleteLinearOrder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
inst✝¹ : Nonempty γ
inst✝ : DenselyOrdered α
a b : α
s t : Set α
hs : IsClosed s
ht : IsClosed t
hab : Icc a b ⊆ t ∪ s
x : α
hx : x ∈ Icc a b ∩ s
y : α
hy : y ∈ Icc a b ∩ t
h : y ≤ x
⊢ Set.Nonempty (Icc a b ∩ (t ∩ s))
[PROOFSTEP]
exact isPreconnected_Icc_aux y x t s h ht hs hab hy hx
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝⁷ : ConditionallyCompleteLinearOrder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
inst✝¹ : Nonempty γ
inst✝ : DenselyOrdered α
a b : α
⊢ {s | IsPreconnected s} =
    range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅})
[PROOFSTEP]
refine' Subset.antisymm setOf_isPreconnected_subset_of_ordered _
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝⁷ : ConditionallyCompleteLinearOrder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
inst✝¹ : Nonempty γ
inst✝ : DenselyOrdered α
a b : α
⊢ range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅}) ⊆
    {s | IsPreconnected s}
[PROOFSTEP]
simp only [subset_def, forall_range_iff, uncurry, or_imp, forall_and, mem_union, mem_setOf_eq, insert_eq,
  mem_singleton_iff, forall_eq, forall_true_iff, and_true_iff, isPreconnected_Icc, isPreconnected_Ico,
  isPreconnected_Ioc, isPreconnected_Ioo, isPreconnected_Ioi, isPreconnected_Iio, isPreconnected_Ici,
  isPreconnected_Iic, isPreconnected_univ, isPreconnected_empty]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝¹⁰ : ConditionallyCompleteLinearOrder α
inst✝⁹ : TopologicalSpace α
inst✝⁸ : OrderTopology α
inst✝⁷ : ConditionallyCompleteLinearOrder β
inst✝⁶ : TopologicalSpace β
inst✝⁵ : OrderTopology β
inst✝⁴ : Nonempty γ
inst✝³ : DenselyOrdered α
a✝ b✝ : α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
a b : α
f : α → δ
hf : ContinuousOn f (uIcc a b)
⊢ uIcc (f a) (f b) ⊆ f '' uIcc a b
[PROOFSTEP]
cases le_total (f a) (f b)
[GOAL]
case inl
α : Type u
β : Type v
γ : Type w
inst✝¹⁰ : ConditionallyCompleteLinearOrder α
inst✝⁹ : TopologicalSpace α
inst✝⁸ : OrderTopology α
inst✝⁷ : ConditionallyCompleteLinearOrder β
inst✝⁶ : TopologicalSpace β
inst✝⁵ : OrderTopology β
inst✝⁴ : Nonempty γ
inst✝³ : DenselyOrdered α
a✝ b✝ : α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
a b : α
f : α → δ
hf : ContinuousOn f (uIcc a b)
h✝ : f a ≤ f b
⊢ uIcc (f a) (f b) ⊆ f '' uIcc a b
[PROOFSTEP]
simp [*, isPreconnected_uIcc.intermediate_value]
[GOAL]
case inr
α : Type u
β : Type v
γ : Type w
inst✝¹⁰ : ConditionallyCompleteLinearOrder α
inst✝⁹ : TopologicalSpace α
inst✝⁸ : OrderTopology α
inst✝⁷ : ConditionallyCompleteLinearOrder β
inst✝⁶ : TopologicalSpace β
inst✝⁵ : OrderTopology β
inst✝⁴ : Nonempty γ
inst✝³ : DenselyOrdered α
a✝ b✝ : α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
a b : α
f : α → δ
hf : ContinuousOn f (uIcc a b)
h✝ : f b ≤ f a
⊢ uIcc (f a) (f b) ⊆ f '' uIcc a b
[PROOFSTEP]
simp [*, isPreconnected_uIcc.intermediate_value]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝¹⁰ : ConditionallyCompleteLinearOrder α
inst✝⁹ : TopologicalSpace α
inst✝⁸ : OrderTopology α
inst✝⁷ : ConditionallyCompleteLinearOrder β
inst✝⁶ : TopologicalSpace β
inst✝⁵ : OrderTopology β
inst✝⁴ : Nonempty γ
inst✝³ : DenselyOrdered α
a✝ b✝ : α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
s : Set α
hs : OrdConnected s
f : α → δ
hf : ContinuousOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
⊢ SurjOn f s (uIcc (f a) (f b))
[PROOFSTEP]
cases' le_total (f a) (f b) with hab hab
[GOAL]
case inl
α : Type u
β : Type v
γ : Type w
inst✝¹⁰ : ConditionallyCompleteLinearOrder α
inst✝⁹ : TopologicalSpace α
inst✝⁸ : OrderTopology α
inst✝⁷ : ConditionallyCompleteLinearOrder β
inst✝⁶ : TopologicalSpace β
inst✝⁵ : OrderTopology β
inst✝⁴ : Nonempty γ
inst✝³ : DenselyOrdered α
a✝ b✝ : α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
s : Set α
hs : OrdConnected s
f : α → δ
hf : ContinuousOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
hab : f a ≤ f b
⊢ SurjOn f s (uIcc (f a) (f b))
[PROOFSTEP]
simp [hf.surjOn_Icc, *]
[GOAL]
case inr
α : Type u
β : Type v
γ : Type w
inst✝¹⁰ : ConditionallyCompleteLinearOrder α
inst✝⁹ : TopologicalSpace α
inst✝⁸ : OrderTopology α
inst✝⁷ : ConditionallyCompleteLinearOrder β
inst✝⁶ : TopologicalSpace β
inst✝⁵ : OrderTopology β
inst✝⁴ : Nonempty γ
inst✝³ : DenselyOrdered α
a✝ b✝ : α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
s : Set α
hs : OrdConnected s
f : α → δ
hf : ContinuousOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
hab : f b ≤ f a
⊢ SurjOn f s (uIcc (f a) (f b))
[PROOFSTEP]
simp [hf.surjOn_Icc, *]


[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