feat(topology/algebra/ordered): list of preconnected sets (#2943)

A subset of a densely ordered conditionally complete lattice (e.g., `ℝ`) with order topology is preconnected if and only if it is one of the intervals.



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

src/data/set/basic.lean

@@ -854,12 +854,23 @@ by rw [union_comm, ←diff_subset_iff]
 @[simp] lemma diff_singleton_subset_iff {x : α} {s t : set α} : s \ {x} ⊆ t ↔ s ⊆ insert x t :=
 by { rw [←union_singleton, union_comm], apply diff_subset_iff }
 
+lemma subset_diff_singleton {x : α} {s t : set α} (h : s ⊆ t) (hx : x ∉ s) : s ⊆ t \ {x} :=
+subset_inter h $ subset_compl_comm.1 $ singleton_subset_iff.2 hx
+
 lemma subset_insert_diff_singleton (x : α) (s : set α) : s ⊆ insert x (s \ {x}) :=
 by rw [←diff_singleton_subset_iff]
 
 lemma diff_subset_comm {s t u : set α} : s \ t ⊆ u ↔ s \ u ⊆ t :=
 by rw [diff_subset_iff, diff_subset_iff, union_comm]
 
+lemma diff_inter {s t u : set α} : s \ (t ∩ u) = (s \ t) ∪ (s \ u) :=
+ext $ λ x, by simp [classical.not_and_distrib, and_or_distrib_left]
+
+lemma diff_compl : s \ -t = s ∩ t := by rw [diff_eq, compl_compl]
+
+lemma diff_diff_right {s t u : set α} : s \ (t \ u) = (s \ t) ∪ (s ∩ u) :=
+by rw [diff_eq t u, diff_inter, diff_compl]
+
 @[simp] theorem insert_diff_of_mem (s) (h : a ∈ t) : insert a s \ t = s \ t :=
 ext $ by intro; constructor; simp [or_imp_distrib, h] {contextual := tt}
 
@@ -897,8 +908,11 @@ by simp [insert_eq, union_diff_self, -union_singleton, -singleton_union]
 
 @[simp] lemma diff_self {s : set α} : s \ s = ∅ := ext $ by simp
 
-lemma mem_diff_singleton {s s' : set α} {t : set (set α)} : s ∈ t \ {s'} ↔ (s ∈ t ∧ s ≠ s') :=
-by simp
+lemma diff_diff_cancel_left {s t : set α} (h : s ⊆ t) : t \ (t \ s) = s :=
+by simp only [diff_diff_right, diff_self, inter_eq_self_of_subset_right h, empty_union]
+
+lemma mem_diff_singleton {x y : α} {s : set α} : x ∈ s \ {y} ↔ (x ∈ s ∧ x ≠ y) :=
+iff.rfl
 
 lemma mem_diff_singleton_empty {s : set α} {t : set (set α)} :
   s ∈ t \ {∅} ↔ (s ∈ t ∧ s.nonempty) :=

src/data/set/intervals/basic.lean

@@ -280,38 +280,81 @@ 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 Ico_diff_Ioo_eq_singleton (h : a < b) : Ico a b \ Ioo a b = {a} :=
-set.ext $ λ x, begin
-  simp [not_and'], split,
-  { rintro ⟨⟨ax, xb⟩, hne⟩,
-    exact (eq_or_lt_of_le ax).elim eq.symm (λ h', absurd h' (hne xb)) },
-  { rintro rfl, exact ⟨⟨le_refl _, h⟩, λ _, lt_irrefl x⟩ }
-end
+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 Ioc_diff_Ioo_eq_singleton (h : a < b) : Ioc a b \ Ioo a b = {b} :=
-set.ext $ λ x, begin
-  simp, split,
-  { rintro ⟨⟨ax, xb⟩, hne⟩,
-    exact (eq_or_lt_of_le xb).elim id (λ h', absurd h' (hne ax)) },
-  { rintro rfl, exact ⟨⟨h, le_refl _⟩, λ _, lt_irrefl x⟩ }
-end
+lemma Icc_diff_right : Icc a b \ {b} = Ico a b :=
+ext $ λ x, by simp [lt_iff_le_and_ne, and_assoc]
 
-lemma Icc_diff_Ico_eq_singleton (h : a ≤ b) : Icc a b \ Ico a b = {b} :=
-set.ext $ λ x, begin
-  simp, split,
-  { rintro ⟨⟨ax, xb⟩, h⟩,
-    exact classical.by_contradiction
-      (λ ne, h ax (lt_of_le_of_ne xb ne)) },
-  { rintro rfl, exact ⟨⟨h, le_refl _⟩, λ _, lt_irrefl x⟩ }
-end
+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 :=
+ext $ λ x, by simp [and_assoc, ← lt_iff_le_and_ne]
+
+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 :=
+ext $ λ x, by simp [lt_iff_le_and_ne, eq_comm]
+
+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} :=
+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} :=
+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} :=
+by rw [← Icc_diff_right, diff_diff_cancel_left (singleton_subset_iff.2 $ right_mem_Icc.2 h)]
 
-lemma Icc_diff_Ioc_eq_singleton (h : a ≤ b) : Icc a b \ Ioc a b = {a} :=
-set.ext $ λ x, begin
-  simp [not_and'], split,
-  { rintro ⟨⟨ax, xb⟩, h⟩,
-    exact classical.by_contradiction
-      (λ hne, h xb (lt_of_le_of_ne ax (ne.symm hne))) },
-  { rintro rfl, exact ⟨⟨le_refl _, h⟩, λ _, lt_irrefl x⟩ }
+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} :=
+by { rw [← Icc_diff_both, diff_diff_cancel_left], simp [insert_subset, h] }
+
+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} :=
+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]
+
+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, 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) :
+  s ∈ ({Iic a, Iio a} : set (set α)) :=
+@mem_Ici_Ioi_of_subset_of_subset (order_dual α) _ a s ho hc
+
+lemma mem_Icc_Ico_Ioc_Ioo_of_subset_of_subset {s : set α} (ho : Ioo a b ⊆ s) (hc : s ⊆ Icc a b) :
+  s ∈ ({Icc a b, Ico a b, Ioc a b, Ioo a b} : set (set α)) :=
+begin
+  classical,
+  by_cases ha : a ∈ s; by_cases hb : b ∈ s,
+  { refine or.inl (subset.antisymm hc _),
+    rwa [← Ico_diff_left, diff_singleton_subset_iff, insert_eq_of_mem ha,
+      ← Icc_diff_right, diff_singleton_subset_iff, insert_eq_of_mem hb] at ho },
+  { refine (or.inr $ or.inl $ subset.antisymm _ _),
+    { rw [← Icc_diff_right],
+      exact subset_diff_singleton hc hb },
+    { rwa [← Ico_diff_left, diff_singleton_subset_iff, insert_eq_of_mem ha] at ho } },
+  { refine (or.inr $ or.inr $ or.inl $ subset.antisymm _ _),
+    { rw [← Icc_diff_left],
+      exact subset_diff_singleton hc ha },
+    { rwa [← Ioc_diff_right, diff_singleton_subset_iff, insert_eq_of_mem hb] at ho } },
+  { refine (or.inr $ or.inr $ or.inr $ subset.antisymm _ ho),
+    rw [← Ico_diff_left, ← Icc_diff_right],
+    apply_rules [subset_diff_singleton] }
 end
 
 end partial_order

src/order/bounds.lean

@@ -57,6 +57,30 @@ lemma mem_upper_bounds : a ∈ upper_bounds s ↔ ∀ x ∈ s, x ≤ a := iff.rf
 
 lemma mem_lower_bounds : a ∈ lower_bounds s ↔ ∀ x ∈ s, a ≤ x := iff.rfl
 
+/-- A set `s` is not bounded above if and only if for each `x` there exists `y ∈ s` such that `x`
+is not greater than or equal to `y`. This version only assumes `preorder` structure and uses
+`¬(y ≤ x)`. A version for linear orders is called `not_bdd_above_iff`. -/
+lemma not_bdd_above_iff' : ¬bdd_above s ↔ ∀ x, ∃ y ∈ s, ¬(y ≤ x) :=
+by simp [bdd_above, upper_bounds, set.nonempty]
+
+/-- A set `s` is not bounded below if and only if for each `x` there exists `y ∈ s` such that `x`
+is not less than or equal to `y`. This version only assumes `preorder` structure and uses
+`¬(x ≤ y)`. A version for linear orders is called `not_bdd_below_iff`. -/
+lemma not_bdd_below_iff' : ¬bdd_below s ↔ ∀ x, ∃ y ∈ s, ¬(x ≤ y) :=
+@not_bdd_above_iff' (order_dual α) _ _
+
+/-- A set `s` is not bounded above if and only if for each `x` there exists `y ∈ s` that is greater
+than `x`. A version for preorders is called `not_bdd_above_iff'`. -/
+lemma not_bdd_above_iff {α : Type*} [linear_order α] {s : set α} :
+  ¬bdd_above s ↔ ∀ x, ∃ y ∈ s, x < y :=
+by simp only [not_bdd_above_iff', not_le]
+
+/-- A set `s` is not bounded below if and only if for each `x` there exists `y ∈ s` that is less
+than `x`. A version for preorders is called `not_bdd_below_iff'`. -/
+lemma not_bdd_below_iff {α : Type*} [linear_order α] {s : set α} :
+  ¬bdd_below s ↔ ∀ x, ∃ y ∈ s, y < x :=
+@not_bdd_above_iff (order_dual α) _ _
+
 /-!
 ### Monotonicity
 -/
@@ -476,6 +500,12 @@ not_le_of_lt ha' this
 lemma is_glb.nonempty [no_top_order α] (hs : is_glb s a) : s.nonempty :=
 @is_lub.nonempty (order_dual α) _ _ _ _ hs
 
+lemma nonempty_of_not_bdd_above [ha : nonempty α] (h : ¬bdd_above s) : s.nonempty :=
+nonempty.elim ha $ λ x, (not_bdd_above_iff'.1 h x).imp $ λ a ha, ha.fst
+
+lemma nonempty_of_not_bdd_below [ha : nonempty α] (h : ¬bdd_below s) : s.nonempty :=
+@nonempty_of_not_bdd_above (order_dual α) _ _ _ h
+
 /-!
 ### insert
 -/