feat(data/set/intervals): define set.ord_connected (#3647)

A set `s : set α`, `[preorder α]` is `ord_connected` if for
any `x y ∈ s` we have `[x, y] ⊆ s`. For real numbers this property
is equivalent to each of the properties `convex s`
and `is_preconnected s`. We define it for any `preorder`, prove some
basic properties, and migrate lemmas like `convex_I??` and
`is_preconnected_I??` to this API.



Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

src/analysis/calculus/darboux.lean

@@ -75,19 +75,19 @@ theorem convex_image_has_deriv_at {s : set ℝ} (hs : convex s)
   (hf : ∀ x ∈ s, has_deriv_at f (f' x) x) :
   convex (f' '' s) :=
 begin
-  refine convex_real_iff.2 _,
-  rintros _ _ ⟨a, ha, rfl⟩ ⟨b, hb, rfl⟩ m ⟨hma, hmb⟩,
+  refine real.convex_iff_ord_connected.2 _,
+  rintros _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩ m ⟨hma, hmb⟩,
   cases eq_or_lt_of_le hma with hma hma,
     by exact hma ▸ mem_image_of_mem f' ha,
   cases eq_or_lt_of_le hmb with hmb hmb,
     by exact hmb.symm ▸ mem_image_of_mem f' hb,
   cases le_total a b with hab hab,
-  { have : Icc a b ⊆ s, from convex_real_iff.1 hs ha hb,
+  { have : Icc a b ⊆ s, from hs.ord_connected ha hb,
     rcases exists_has_deriv_within_at_eq_of_gt_of_lt hab
       (λ x hx, (hf x $ this hx).has_deriv_within_at) hma hmb
       with ⟨c, cmem, hc⟩,
     exact ⟨c, this cmem, hc⟩ },
-  { have : Icc b a ⊆ s, from convex_real_iff.1 hs hb ha,
+  { have : Icc b a ⊆ s, from hs.ord_connected hb ha,
     rcases exists_has_deriv_within_at_eq_of_lt_of_gt hab
       (λ x hx, (hf x $ this hx).has_deriv_within_at) hmb hma
       with ⟨c, cmem, hc⟩,
@@ -102,6 +102,6 @@ theorem deriv_forall_lt_or_forall_gt_of_forall_ne {s : set ℝ} (hs : convex s)
 begin
   contrapose! hf',
   rcases hf' with ⟨⟨b, hb, hmb⟩, ⟨a, ha, hma⟩⟩,
-  exact convex_real_iff.1 (convex_image_has_deriv_at hs hf) (mem_image_of_mem f' ha)
+  exact (convex_image_has_deriv_at hs hf).ord_connected (mem_image_of_mem f' ha)
     (mem_image_of_mem f' hb) ⟨hma, hmb⟩
 end

src/analysis/calculus/mean_value.lean

@@ -612,7 +612,7 @@ theorem convex.mul_sub_lt_image_sub_of_lt_deriv {D : set ℝ} (hD : convex D) {f
   ∀ x y ∈ D, x < y → C * (y - x) < f y - f x :=
 begin
   assume x y hx hy hxy,
-  have hxyD : Icc x y ⊆ D, from convex_real_iff.1 hD hx hy,
+  have hxyD : Icc x y ⊆ D, from hD.ord_connected hx hy,
   have hxyD' : Ioo x y ⊆ interior D,
     from subset_sUnion_of_mem ⟨is_open_Ioo, subset.trans Ioo_subset_Icc_self hxyD⟩,
   obtain ⟨a, a_mem, ha⟩ : ∃ a ∈ Ioo x y, deriv f a = (f y - f x) / (y - x),
@@ -640,7 +640,7 @@ theorem convex.mul_sub_le_image_sub_of_le_deriv {D : set ℝ} (hD : convex D) {f
 begin
   assume x y hx hy hxy,
   cases eq_or_lt_of_le hxy with hxy' hxy', by rw [hxy', sub_self, sub_self, mul_zero],
-  have hxyD : Icc x y ⊆ D, from convex_real_iff.1 hD hx hy,
+  have hxyD : Icc x y ⊆ D, from hD.ord_connected hx hy,
   have hxyD' : Ioo x y ⊆ interior D,
     from subset_sUnion_of_mem ⟨is_open_Ioo, subset.trans Ioo_subset_Icc_self hxyD⟩,
   obtain ⟨a, a_mem, ha⟩ : ∃ a ∈ Ioo x y, deriv f a = (f y - f x) / (y - x),
@@ -785,7 +785,7 @@ convex_on_real_of_slope_mono_adjacent hD
 begin
   intros x y z hx hz hxy hyz,
   -- First we prove some trivial inclusions
-  have hxzD : Icc x z ⊆ D, from convex_real_iff.1 hD hx hz,
+  have hxzD : Icc x z ⊆ D, from hD.ord_connected hx hz,
   have hxyD : Icc x y ⊆ D, from subset.trans (Icc_subset_Icc_right $ le_of_lt hyz) hxzD,
   have hxyD' : Ioo x y ⊆ interior D,
     from subset_sUnion_of_mem ⟨is_open_Ioo, subset.trans Ioo_subset_Icc_self hxyD⟩,

src/analysis/convex/basic.lean

@@ -3,7 +3,7 @@ Copyright (c) 2019 Alexander Bentkamp. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Alexander Bentkamp, Yury Kudriashov
 -/
-import data.set.intervals.unordered_interval
+import data.set.intervals.ord_connected
 import data.set.intervals.image_preimage
 import data.complex.module
 import linear_algebra.affine_space
@@ -289,40 +289,23 @@ by simpa only [add_comm] using hs.translate_preimage_right a
 lemma convex.affinity (hs : convex s) (z : E) (c : ℝ) : convex ((λx, z + c • x) '' s) :=
 hs.affine_image $ affine_map.const ℝ E E E z +ᵥ c • affine_map.id ℝ E E
 
-lemma convex_real_iff {s : set ℝ} :
-  convex s ↔ ∀ {x y}, x ∈ s → y ∈ s → Icc x y ⊆ s :=
+lemma real.convex_iff_ord_connected {s : set ℝ} : convex s ↔ ord_connected s :=
 begin
-  simp only [convex_iff_segment_subset, segment_eq_Icc'],
-  split; intros h x y hx hy,
-  { cases le_or_lt x y with hxy hxy,
-    { simpa [hxy] using h hx hy },
-    { simp [hxy] } },
-  { apply h; cases le_total x y; simp [*] }
+  simp only [convex_iff_segment_subset, segment_eq_interval, ord_connected_iff_interval_subset],
+  exact forall_congr (λ x, forall_swap)
 end
 
-lemma convex_Iio (r : ℝ) : convex (Iio r) :=
-convex_real_iff.2 $ λ x y hx hy z hz, lt_of_le_of_lt hz.2 hy
+alias real.convex_iff_ord_connected ↔ convex.ord_connected set.ord_connected.convex
 
-lemma convex_Ioi (r : ℝ) : convex (Ioi r) :=
-convex_real_iff.2 $ λ x y hx hy z hz, lt_of_lt_of_le hx hz.1
-
-lemma convex_Iic (r : ℝ) : convex (Iic r) :=
-convex_real_iff.2 $ λ x y hx hy z hz, le_trans hz.2 hy
-
-lemma convex_Ici (r : ℝ) : convex (Ici r) :=
-convex_real_iff.2 $ λ x y hx hy z hz, le_trans hx hz.1
-
-lemma convex_Ioo (r : ℝ) (s : ℝ) : convex (Ioo r s) :=
-(convex_Ioi _).inter (convex_Iio _)
-
-lemma convex_Ico (r : ℝ) (s : ℝ) : convex (Ico r s) :=
-(convex_Ici _).inter (convex_Iio _)
-
-lemma convex_Ioc (r : ℝ) (s : ℝ) : convex (Ioc r s) :=
-(convex_Ioi _).inter (convex_Iic _)
-
-lemma convex_Icc (r : ℝ) (s : ℝ) : convex (Icc r s) :=
-(convex_Ici _).inter (convex_Iic _)
+lemma convex_Iio (r : ℝ) : convex (Iio r) := ord_connected_Iio.convex
+lemma convex_Ioi (r : ℝ) : convex (Ioi r) := ord_connected_Ioi.convex
+lemma convex_Iic (r : ℝ) : convex (Iic r) := ord_connected_Iic.convex
+lemma convex_Ici (r : ℝ) : convex (Ici r) := ord_connected_Ici.convex
+lemma convex_Ioo (r s : ℝ) : convex (Ioo r s) := ord_connected_Ioo.convex
+lemma convex_Ico (r s : ℝ) : convex (Ico r s) := ord_connected_Ico.convex
+lemma convex_Ioc (r : ℝ) (s : ℝ) : convex (Ioc r s) := ord_connected_Ioc.convex
+lemma convex_Icc (r : ℝ) (s : ℝ) : convex (Icc r s) := ord_connected_Icc.convex
+lemma convex_interval (r : ℝ) (s : ℝ) : convex (interval r s) := ord_connected_interval.convex
 
 lemma convex_segment (a b : E) : convex [a, b] :=
 begin
@@ -388,7 +371,7 @@ lemma convex.combo_self (a : α) {x y : α} (h : x + y = 1) : a = x * a + y * a
       ... = (x + y) * a     : by rw [h]
       ... = x * a + y * a   : by rw [add_mul]
 
-/-
+/--
 If x is in an Ioo, it can be expressed as a convex combination of the endpoints.
 -/
 lemma convex.mem_Ioo {a b x : α} (h : a < b) :

src/analysis/convex/topology.lean

@@ -28,6 +28,11 @@ variables {ι : Type*} {E : Type*}
 
 open set
 
+lemma real.convex_iff_is_preconnected {s : set ℝ} : convex s ↔ is_preconnected s :=
+real.convex_iff_ord_connected.trans is_preconnected_iff_ord_connected.symm
+
+alias real.convex_iff_is_preconnected ↔ convex.is_preconnected is_preconnected.convex
+
 /-! ### Standard simplex -/
 
 section std_simplex

src/data/set/intervals/basic.lean

@@ -288,56 +288,56 @@ variables {α : Type u} [partial_order α] {a b : α}
 @[simp] lemma Icc_self (a : α) : Icc a a = {a} :=
 set.ext $ by simp [Icc, le_antisymm_iff, and_comm]
 
-lemma Icc_diff_left : Icc a b \ {a} = Ioc a b :=
+@[simp] lemma Icc_diff_left : Icc a b \ {a} = Ioc a b :=
 ext $ λ x, by simp [lt_iff_le_and_ne, eq_comm, and.right_comm]
 
-lemma Icc_diff_right : Icc a b \ {b} = Ico a b :=
+@[simp] lemma Icc_diff_right : Icc a b \ {b} = Ico a b :=
 ext $ λ x, by simp [lt_iff_le_and_ne, and_assoc]
 
-lemma Ico_diff_left : Ico a b \ {a} = Ioo a b :=
+@[simp] lemma Ico_diff_left : Ico a b \ {a} = Ioo a b :=
 ext $ λ x, by simp [and.right_comm, ← lt_iff_le_and_ne, eq_comm]
 
-lemma Ioc_diff_right : Ioc a b \ {b} = Ioo a b :=
+@[simp] lemma Ioc_diff_right : Ioc a b \ {b} = Ioo a b :=
 ext $ λ x, by simp [and_assoc, ← lt_iff_le_and_ne]
 
-lemma Icc_diff_both : Icc a b \ {a, b} = Ioo a b :=
+@[simp] lemma Icc_diff_both : Icc a b \ {a, b} = Ioo a b :=
 by rw [insert_eq, ← diff_diff, Icc_diff_left, Ioc_diff_right]
 
-lemma Ici_diff_left : Ici a \ {a} = Ioi a :=
+@[simp] lemma Ici_diff_left : Ici a \ {a} = Ioi a :=
 ext $ λ x, by simp [lt_iff_le_and_ne, eq_comm]
 
-lemma Iic_diff_right : Iic a \ {a} = Iio a :=
+@[simp] lemma Iic_diff_right : Iic a \ {a} = Iio a :=
 ext $ λ x, by simp [lt_iff_le_and_ne]
 
-lemma Ico_diff_Ioo_same (h : a < b) : Ico a b \ Ioo a b = {a} :=
+@[simp] lemma Ico_diff_Ioo_same (h : a < b) : Ico a b \ Ioo a b = {a} :=
 by rw [← Ico_diff_left, diff_diff_cancel_left (singleton_subset_iff.2 $ left_mem_Ico.2 h)]
 
-lemma Ioc_diff_Ioo_same (h : a < b) : Ioc a b \ Ioo a b = {b} :=
+@[simp] lemma Ioc_diff_Ioo_same (h : a < b) : Ioc a b \ Ioo a b = {b} :=
 by rw [← Ioc_diff_right, diff_diff_cancel_left (singleton_subset_iff.2 $ right_mem_Ioc.2 h)]
 
-lemma Icc_diff_Ico_same (h : a ≤ b) : Icc a b \ Ico a b = {b} :=
+@[simp] lemma Icc_diff_Ico_same (h : a ≤ b) : Icc a b \ Ico a b = {b} :=
 by rw [← Icc_diff_right, diff_diff_cancel_left (singleton_subset_iff.2 $ right_mem_Icc.2 h)]
 
-lemma Icc_diff_Ioc_same (h : a ≤ b) : Icc a b \ Ioc a b = {a} :=
+@[simp] lemma Icc_diff_Ioc_same (h : a ≤ b) : Icc a b \ Ioc a b = {a} :=
 by rw [← Icc_diff_left, diff_diff_cancel_left (singleton_subset_iff.2 $ left_mem_Icc.2 h)]
 
-lemma Icc_diff_Ioo_same (h : a ≤ b) : Icc a b \ Ioo a b = {a, b} :=
+@[simp] lemma Icc_diff_Ioo_same (h : a ≤ b) : Icc a b \ Ioo a b = {a, b} :=
 by { rw [← Icc_diff_both, diff_diff_cancel_left], simp [insert_subset, h] }
 
-lemma Ici_diff_Ioi_same : Ici a \ Ioi a = {a} :=
+@[simp] lemma Ici_diff_Ioi_same : Ici a \ Ioi a = {a} :=
 by rw [← Ici_diff_left, diff_diff_cancel_left (singleton_subset_iff.2 left_mem_Ici)]
 
-lemma Iic_diff_Iio_same : Iic a \ Iio a = {a} :=
+@[simp] lemma Iic_diff_Iio_same : Iic a \ Iio a = {a} :=
 by rw [← Iic_diff_right, diff_diff_cancel_left (singleton_subset_iff.2 right_mem_Iic)]
 
-lemma Ioi_union_left : Ioi a ∪ {a} = Ici a := ext $ λ x, by simp [eq_comm, le_iff_eq_or_lt]
+@[simp] lemma Ioi_union_left : Ioi a ∪ {a} = Ici a := ext $ λ x, by simp [eq_comm, le_iff_eq_or_lt]
 
-lemma Iio_union_right : Iio a ∪ {a} = Iic a := ext $ λ x, le_iff_lt_or_eq.symm
+@[simp] lemma Iio_union_right : Iio a ∪ {a} = Iic a := ext $ λ x, le_iff_lt_or_eq.symm
 
 lemma mem_Ici_Ioi_of_subset_of_subset {s : set α} (ho : Ioi a ⊆ s) (hc : s ⊆ Ici a) :
   s ∈ ({Ici a, Ioi a} : set (set α)) :=
 classical.by_cases
-  (λ h : a ∈ s, or.inl $ subset.antisymm hc $ by simp [← Ioi_union_left, insert_subset, *])
+  (λ h : a ∈ s, or.inl $ subset.antisymm hc $ by rw [← Ioi_union_left, union_subset_iff]; simp *)
   (λ h, or.inr $ subset.antisymm (λ x hx, lt_of_le_of_ne (hc hx) (λ heq, h $ heq.symm ▸ hx)) ho)
 
 lemma mem_Iic_Iio_of_subset_of_subset {s : set α} (ho : Iio a ⊆ s) (hc : s ⊆ Iic a) :

src/data/set/intervals/ord_connected.lean

@@ -0,0 +1,108 @@
+/-
+Copyright (c) 2020 Yury G. Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Yury G. Kudryashov
+-/
+import data.set.intervals.unordered_interval
+import data.set.lattice
+
+/-!
+# Order-connected sets
+
+We say that a set `s : set α` is `ord_connected` if for all `x y ∈ s` it includes the
+interval `[x, y]`. If `α` is a `densely_ordered` `conditionally_complete_linear_order` with
+the `order_topology`, then this condition is equivalent to `is_preconnected s`. If `α = ℝ`, then
+this condition is also equivalent to `convex s`.
+
+In this file we prove that intersection of a family of `ord_connected` sets is `ord_connected` and
+that all standard intervals are `ord_connected`.
+-/
+
+namespace set
+
+variables {α : Type*} [preorder α] {s t : set α}
+
+/--
+We say that a set `s : set α` is `ord_connected` if for all `x y ∈ s` it includes the
+interval `[x, y]`. If `α` is a `densely_ordered` `conditionally_complete_linear_order` with
+the `order_topology`, then this condition is equivalent to `is_preconnected s`. If `α = ℝ`, then
+this condition is also equivalent to `convex s`.
+-/
+def ord_connected (s : set α) : Prop := ∀ ⦃x⦄ (hx : x ∈ s) ⦃y⦄ (hy : y ∈ s), Icc x y ⊆ s
+
+/-- It suffices to prove `[x, y] ⊆ s` for `x y ∈ s`, `x ≤ y`. -/
+lemma ord_connected_iff : ord_connected s ↔ ∀ (x ∈ s) (y ∈ s), x ≤ y → Icc x y ⊆ s :=
+⟨λ hs x hx y hy hxy, hs hx hy, λ H x hx y hy z hz, H x hx y hy (le_trans hz.1 hz.2) hz⟩
+
+lemma ord_connected_of_Ioo {α : Type*} [partial_order α] {s : set α}
+  (hs : ∀ (x ∈ s) (y ∈ s), x < y → Ioo x y ⊆ s) :
+  ord_connected s :=
+begin
+  rw ord_connected_iff,
+  intros x hx y hy hxy,
+  rcases eq_or_lt_of_le hxy with rfl|hxy', { simpa },
+  have := hs x hx y hy hxy',
+  rw [← union_diff_cancel Ioo_subset_Icc_self],
+  simp [*, insert_subset]
+end
+
+lemma ord_connected.inter {s t : set α} (hs : ord_connected s) (ht : ord_connected t) :
+  ord_connected (s ∩ t) :=
+λ x hx y hy, subset_inter (hs hx.1 hy.1) (ht hx.2 hy.2)
+
+lemma ord_connected.dual {s : set α} (hs : ord_connected s) : @ord_connected (order_dual α) _ s :=
+λ x hx y hy z hz, hs hy hx ⟨hz.2, hz.1⟩
+
+lemma ord_connected_dual {s : set α} : @ord_connected (order_dual α) _ s ↔ ord_connected s :=
+⟨λ h, h.dual, λ h, h.dual⟩
+
+lemma ord_connected_sInter {S : set (set α)} (hS : ∀ s ∈ S, ord_connected s) :
+  ord_connected (⋂₀ S) :=
+λ x hx y hy, subset_sInter $ λ s hs, hS s hs (hx s hs) (hy s hs)
+
+lemma ord_connected_Inter {ι : Sort*} {s : ι → set α} (hs : ∀ i, ord_connected (s i)) :
+  ord_connected (⋂ i, s i) :=
+ord_connected_sInter $ forall_range_iff.2 hs
+
+lemma ord_connected_bInter {ι : Sort*} {p : ι → Prop} {s : Π (i : ι) (hi : p i), set α}
+  (hs : ∀ i hi, ord_connected (s i hi)) :
+  ord_connected (⋂ i hi, s i hi) :=
+ord_connected_Inter $ λ i, ord_connected_Inter $ hs i
+
+lemma ord_connected_Ici {a : α} : ord_connected (Ici a) := λ x hx y hy z hz, le_trans hx hz.1
+lemma ord_connected_Iic {a : α} : ord_connected (Iic a) := λ x hx y hy z hz, le_trans hz.2 hy
+lemma ord_connected_Ioi {a : α} : ord_connected (Ioi a) := λ x hx y hy z hz, lt_of_lt_of_le hx hz.1
+lemma ord_connected_Iio {a : α} : ord_connected (Iio a) := λ x hx y hy z hz, lt_of_le_of_lt hz.2 hy
+
+lemma ord_connected_Icc {a b : α} : ord_connected (Icc a b) :=
+ord_connected_Ici.inter ord_connected_Iic
+
+lemma ord_connected_Ico {a b : α} : ord_connected (Ico a b) :=
+ord_connected_Ici.inter ord_connected_Iio
+
+lemma ord_connected_Ioc {a b : α} : ord_connected (Ioc a b) :=
+ord_connected_Ioi.inter ord_connected_Iic
+
+lemma ord_connected_Ioo {a b : α} : ord_connected (Ioo a b) :=
+ord_connected_Ioi.inter ord_connected_Iio
+
+lemma ord_connected_empty : ord_connected (∅ : set α) := λ x, false.elim
+
+lemma ord_connected_univ : ord_connected (univ : set α) := λ _ _ _ _, subset_univ _
+
+variables {β : Type*} [decidable_linear_order β]
+
+lemma ord_connected_interval {a b : β} : ord_connected (interval a b) :=
+ord_connected_Icc
+
+lemma ord_connected.interval_subset {s : set β} (hs : ord_connected s)
+  ⦃x⦄ (hx : x ∈ s) ⦃y⦄ (hy : y ∈ s) :
+  interval x y ⊆ s :=
+by cases le_total x y; simp only [interval_of_le, interval_of_ge, *]; apply hs; assumption
+
+lemma ord_connected_iff_interval_subset {s : set β} :
+  ord_connected s ↔ ∀ ⦃x⦄ (hx : x ∈ s) ⦃y⦄ (hy : y ∈ s), interval x y ⊆ s :=
+⟨λ h, h.interval_subset,
+  λ h, ord_connected_iff.2 $ λ x hx y hy hxy, by simpa only [interval_of_le hxy] using h hx hy⟩
+
+end set

src/topology/algebra/ordered.lean

@@ -6,6 +6,7 @@ Authors: Johannes Hölzl, Mario Carneiro, Yury Kudryashov
 import tactic.tfae
 import order.liminf_limsup
 import data.set.intervals.image_preimage
+import data.set.intervals.ord_connected
 import topology.algebra.group
 
 /-!
@@ -1770,38 +1771,28 @@ begin
   exact λ w ⟨wt, wzy⟩, (this wzy).elim id (λ h, (wt h).elim)
 end
 
-lemma is_preconnected_iff_forall_Icc_subset {s : set α} :
-  is_preconnected s ↔ ∀ x y ∈ s, x ≤ y → Icc x y ⊆ s :=
-⟨λ h x y hx hy hxy, h.Icc_subset hx hy, λ h, is_preconnected_of_forall_pair $ λ x y hx hy,
-  ⟨Icc (min x y) (max x y), h (min x y) (max x y)
-    ((min_choice x y).elim (λ h', by rwa h') (λ h', by rwa h'))
-    ((max_choice x y).elim (λ h', by rwa h') (λ h', by rwa h')) min_le_max,
-    ⟨min_le_left x y, le_max_left x y⟩, ⟨min_le_right x y, le_max_right x y⟩, is_preconnected_Icc⟩⟩
+lemma is_preconnected_interval : is_preconnected (interval a b) := is_preconnected_Icc
 
-lemma is_preconnected_Ici : is_preconnected (Ici a) :=
-is_preconnected_iff_forall_Icc_subset.2 $ λ x y hx hy hxy, (Icc_subset_Ici_iff hxy).2 hx
+lemma is_preconnected_iff_ord_connected {s : set α} :
+  is_preconnected s ↔ ord_connected s :=
+⟨λ h x hx y hy, h.Icc_subset hx hy, λ h, is_preconnected_of_forall_pair $ λ x y hx hy,
+  ⟨interval x y, h.interval_subset hx hy, left_mem_interval, right_mem_interval,
+    is_preconnected_interval⟩⟩
 
-lemma is_preconnected_Iic : is_preconnected (Iic a) :=
-is_preconnected_iff_forall_Icc_subset.2 $ λ x y hx hy hxy, (Icc_subset_Iic_iff hxy).2 hy
+alias is_preconnected_iff_ord_connected ↔
+  is_preconnected.ord_connected set.ord_connected.is_preconnected
 
-lemma is_preconnected_Iio : is_preconnected (Iio a) :=
-is_preconnected_iff_forall_Icc_subset.2 $ λ x y hx hy hxy, (Icc_subset_Iio_iff hxy).2 hy
-
-lemma is_preconnected_Ioi : is_preconnected (Ioi a) :=
-is_preconnected_iff_forall_Icc_subset.2 $ λ x y hx hy hxy, (Icc_subset_Ioi_iff hxy).2 hx
-
-lemma is_preconnected_Ioo : is_preconnected (Ioo a b) :=
-is_preconnected_iff_forall_Icc_subset.2 $ λ x y hx hy hxy, (Icc_subset_Ioo_iff hxy).2 ⟨hx.1, hy.2⟩
-
-lemma is_preconnected_Ioc : is_preconnected (Ioc a b) :=
-is_preconnected_iff_forall_Icc_subset.2 $ λ x y hx hy hxy, (Icc_subset_Ioc_iff hxy).2 ⟨hx.1, hy.2⟩
-
-lemma is_preconnected_Ico : is_preconnected (Ico a b) :=
-is_preconnected_iff_forall_Icc_subset.2 $ λ x y hx hy hxy, (Icc_subset_Ico_iff hxy).2 ⟨hx.1, hy.2⟩
+lemma is_preconnected_Ici : is_preconnected (Ici a) := ord_connected_Ici.is_preconnected
+lemma is_preconnected_Iic : is_preconnected (Iic a) := ord_connected_Iic.is_preconnected
+lemma is_preconnected_Iio : is_preconnected (Iio a) := ord_connected_Iio.is_preconnected
+lemma is_preconnected_Ioi : is_preconnected (Ioi a) := ord_connected_Ioi.is_preconnected
+lemma is_preconnected_Ioo : is_preconnected (Ioo a b) := ord_connected_Ioo.is_preconnected
+lemma is_preconnected_Ioc : is_preconnected (Ioc a b) := ord_connected_Ioc.is_preconnected
+lemma is_preconnected_Ico : is_preconnected (Ico a b) := ord_connected_Ico.is_preconnected
 
 @[priority 100]
 instance ordered_connected_space : preconnected_space α :=
-⟨is_preconnected_iff_forall_Icc_subset.2 $ λ x y hx hy hxy, subset_univ _⟩
+⟨ord_connected_univ.is_preconnected⟩
 
 /-- In a dense conditionally complete linear order, the set of preconnected sets is exactly
 the set of the intervals `Icc`, `Ico`, `Ioc`, `Ioo`, `Ici`, `Ioi`, `Iic`, `Iio`, `(-∞, +∞)`,