feat(order/conditionally_complete_lattice, topology/algebra/ordered): inherited order properties for ord_connected subset (#3991)

If `α` is `densely_ordered`, then so is the subtype `s`, for any `ord_connected` subset `s` of `α`.

Same result for `order_topology`.

Same result for `conditionally_complete_linear_order`, under the hypothesis `inhabited s`.

Author: hrmacbeth

src/data/set/intervals/ord_connected.lean

@@ -29,6 +29,7 @@ the `order_topology`, then this condition is equivalent to `is_preconnected s`.
 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
+attribute [class] ord_connected
 
 /-- 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 :=
@@ -86,6 +87,9 @@ 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
 
+attribute [instance] ord_connected_Ici ord_connected_Iic ord_connected_Ioi ord_connected_Iio
+ord_connected_Icc ord_connected_Ico ord_connected_Ioc ord_connected_Ioo
+
 lemma ord_connected_singleton {α : Type*} [partial_order α] {a : α} :
   ord_connected ({a} : set α) :=
 by { rw ← Icc_self, exact ord_connected_Icc }
@@ -94,6 +98,17 @@ lemma ord_connected_empty : ord_connected (∅ : set α) := λ x, false.elim
 
 lemma ord_connected_univ : ord_connected (univ : set α) := λ _ _ _ _, subset_univ _
 
+/-- In a dense order `α`, the subtype from an `ord_connected` set is also densely ordered. -/
+instance [densely_ordered α] {s : set α} [hs : ord_connected s] :
+  densely_ordered s :=
+⟨ begin
+    intros a₁ a₂ ha,
+    have ha' : ↑a₁ < ↑a₂ := ha,
+    obtain ⟨x, ha₁x, hxa₂⟩ := dense ha',
+    refine ⟨⟨x, _⟩, ⟨ha₁x, hxa₂⟩⟩,
+    exact (hs a₁.2 a₂.2) (Ioo_subset_Icc_self ⟨ha₁x, hxa₂⟩),
+  end ⟩
+
 variables {β : Type*} [decidable_linear_order β]
 
 lemma ord_connected_interval {a b : β} : ord_connected (interval a b) :=

src/order/basic.lean

@@ -341,6 +341,8 @@ instance subtype.decidable_linear_order {α} [decidable_linear_order α] (p : α
   decidable_linear_order (subtype p) :=
 decidable_linear_order.lift subtype.val subtype.val_injective
 
+lemma strict_mono_coe [preorder α] (t : set α) : strict_mono (coe : (subtype t) → α) := λ x y, id
+
 instance prod.has_le (α : Type u) (β : Type v) [has_le α] [has_le β] : has_le (α × β) :=
 ⟨λp q, p.1 ≤ q.1 ∧ p.2 ≤ q.2⟩
 

src/order/conditionally_complete_lattice.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 -/
 import data.nat.enat
+import data.set.intervals.ord_connected
 
 /-!
 # Theory of conditionally complete lattices.
@@ -607,6 +608,30 @@ instance (α : Type*) [conditionally_complete_linear_order α] :
 
 end order_dual
 
+namespace monotone
+variables [preorder α] [conditionally_complete_lattice β] {f : α → β} (h_mono : monotone f)
+
+/-! A monotone function into a conditionally complete lattice preserves the ordering properties of
+`Sup` and `Inf`. -/
+
+lemma le_cSup_image {s : set α} {c : α} (hcs : c ∈ s) (h_bdd : bdd_above s) :
+  f c ≤ Sup (f '' s) :=
+le_cSup (map_bdd_above h_mono h_bdd) (mem_image_of_mem f hcs)
+
+lemma cSup_image_le {s : set α} (hs : s.nonempty) {B : α} (hB: B ∈ upper_bounds s) :
+  Sup (f '' s) ≤ f B :=
+cSup_le (nonempty.image f hs) (h_mono.mem_upper_bounds_image hB)
+
+lemma cInf_image_le {s : set α} {c : α} (hcs : c ∈ s) (h_bdd : bdd_below s) :
+  Inf (f '' s) ≤ f c :=
+@le_cSup_image (order_dual α) (order_dual β) _ _ _ (λ x y hxy, h_mono hxy) _ _ hcs h_bdd
+
+lemma le_cInf_image {s : set α} (hs : s.nonempty) {B : α} (hB: B ∈ lower_bounds s) :
+  f B ≤ Inf (f '' s) :=
+@cSup_image_le (order_dual α) (order_dual β) _ _ _ (λ x y hxy, h_mono hxy) _ hs _ hB
+
+end monotone
+
 section with_top_bot
 
 /-!
@@ -692,3 +717,141 @@ noncomputable instance with_top.with_bot.complete_lattice {α : Type*}
   ..with_top.with_bot.bounded_lattice }
 
 end with_top_bot
+
+section subtype
+variables (s : set α)
+
+/-! ### Subtypes of conditionally complete linear orders
+
+In this section we give conditions on a subset of a conditionally complete linear order, to ensure
+that the subtype is itself conditionally complete.
+
+We check that an `ord_connected` set satisfies these conditions.
+
+TODO There are several possible variants; the `conditionally_complete_linear_order` could be changed
+to `conditionally_complete_linear_order_bot` or `complete_linear_order`.
+-/
+
+open_locale classical
+
+section has_Sup
+variables [has_Sup α]
+
+/-- `has_Sup` structure on a nonempty subset `s` of an object with `has_Sup`. This definition is
+non-canonical (it uses `default s`); it should be used only as here, as an auxiliary instance in the
+construction of the `conditionally_complete_linear_order` structure. -/
+noncomputable def subset_has_Sup [inhabited s] : has_Sup s := {Sup := λ t,
+if ht : Sup (coe '' t : set α) ∈ s then ⟨Sup (coe '' t : set α), ht⟩ else default s}
+
+local attribute [instance] subset_has_Sup
+
+@[simp] lemma subset_Sup_def [inhabited s] :
+  @Sup s _ = λ t,
+  if ht : Sup (coe '' t : set α) ∈ s then ⟨Sup (coe '' t : set α), ht⟩ else default s :=
+rfl
+
+lemma subset_Sup_of_within [inhabited s] {t : set s} (h : Sup (coe '' t : set α) ∈ s) :
+  Sup (coe '' t : set α) = (@Sup s _ t : α) :=
+by simp [dif_pos h]
+
+end has_Sup
+
+section has_Inf
+variables [has_Inf α]
+
+/-- `has_Inf` structure on a nonempty subset `s` of an object with `has_Inf`. This definition is
+non-canonical (it uses `default s`); it should be used only as here, as an auxiliary instance in the
+construction of the `conditionally_complete_linear_order` structure. -/
+noncomputable def subset_has_Inf [inhabited s] : has_Inf s := {Inf := λ t,
+if ht : Inf (coe '' t : set α) ∈ s then ⟨Inf (coe '' t : set α), ht⟩ else default s}
+
+local attribute [instance] subset_has_Inf
+
+@[simp] lemma subset_Inf_def [inhabited s] :
+  @Inf s _ = λ t,
+  if ht : Inf (coe '' t : set α) ∈ s then ⟨Inf (coe '' t : set α), ht⟩ else default s :=
+rfl
+
+lemma subset_Inf_of_within [inhabited s] {t : set s} (h : Inf (coe '' t : set α) ∈ s) :
+  Inf (coe '' t : set α) = (@Inf s _ t : α) :=
+by simp [dif_pos h]
+
+end has_Inf
+
+variables [conditionally_complete_linear_order α]
+
+local attribute [instance] subset_has_Sup
+local attribute [instance] subset_has_Inf
+
+/-- For a nonempty subset of a conditionally complete linear order to be a conditionally complete
+linear order, it suffices that it contain the `Sup` of all its nonempty bounded-above subsets, and
+the `Inf` of all its nonempty bounded-below subsets. -/
+noncomputable def subset_conditionally_complete_linear_order [inhabited s]
+  (h_Sup : ∀ {t : set s} (ht : t.nonempty) (h_bdd : bdd_above t), Sup (coe '' t : set α) ∈ s)
+  (h_Inf : ∀ {t : set s} (ht : t.nonempty) (h_bdd : bdd_below t), Inf (coe '' t : set α) ∈ s) :
+  conditionally_complete_linear_order s :=
+{ le_cSup := begin
+    rintros t c h_bdd hct,
+    -- The following would be a more natural way to finish, but gives a "deep recursion" error:
+    -- simpa [subset_Sup_of_within (h_Sup t)] using (strict_mono_coe s).monotone.le_cSup_image hct h_bdd,
+    have := (strict_mono_coe s).monotone.le_cSup_image hct h_bdd,
+    rwa subset_Sup_of_within s (h_Sup ⟨c, hct⟩ h_bdd) at this,
+  end,
+  cSup_le := begin
+    rintros t B ht hB,
+    have := (strict_mono_coe s).monotone.cSup_image_le ht hB,
+    rwa subset_Sup_of_within s (h_Sup ht ⟨B, hB⟩) at this,
+  end,
+  le_cInf := begin
+    intros t B ht hB,
+    have := (strict_mono_coe s).monotone.le_cInf_image ht hB,
+    rwa subset_Inf_of_within s (h_Inf ht ⟨B, hB⟩) at this,
+  end,
+  cInf_le := begin
+    rintros t c h_bdd hct,
+    have := (strict_mono_coe s).monotone.cInf_image_le hct h_bdd,
+    rwa subset_Inf_of_within s (h_Inf ⟨c, hct⟩ h_bdd) at this,
+  end,
+  ..subset_has_Sup s,
+  ..subset_has_Inf s,
+  ..distrib_lattice.to_lattice s,
+  ..classical.DLO s }
+
+section ord_connected
+
+/-- The `Sup` function on a nonempty `ord_connected` set `s` in a conditionally complete linear
+order takes values within `s`, for all nonempty bounded-above subsets of `s`. -/
+lemma Sup_within_of_ord_connected
+  {s : set α} [hs : ord_connected s] ⦃t : set s⦄ (ht : t.nonempty) (h_bdd : bdd_above t) :
+  Sup (coe '' t : set α) ∈ s :=
+begin
+  obtain ⟨c, hct⟩ : ∃ c, c ∈ t := ht,
+  obtain ⟨B, hB⟩ : ∃ B, B ∈ upper_bounds t := h_bdd,
+  refine hs c.2 B.2 ⟨_, _⟩,
+  { exact (strict_mono_coe s).monotone.le_cSup_image hct ⟨B, hB⟩ },
+  { exact (strict_mono_coe s).monotone.cSup_image_le ⟨c, hct⟩ hB },
+end
+
+/-- The `Inf` function on a nonempty `ord_connected` set `s` in a conditionally complete linear
+order takes values within `s`, for all nonempty bounded-below subsets of `s`. -/
+lemma Inf_within_of_ord_connected
+  {s : set α} [hs : ord_connected s] ⦃t : set s⦄ (ht : t.nonempty) (h_bdd : bdd_below t) :
+  Inf (coe '' t : set α) ∈ s :=
+begin
+  obtain ⟨c, hct⟩ : ∃ c, c ∈ t := ht,
+  obtain ⟨B, hB⟩ : ∃ B, B ∈ lower_bounds t := h_bdd,
+  refine hs B.2 c.2 ⟨_, _⟩,
+  { exact (strict_mono_coe s).monotone.le_cInf_image ⟨c, hct⟩ hB },
+  { exact (strict_mono_coe s).monotone.cInf_image_le hct ⟨B, hB⟩ },
+end
+
+/-- A nonempty `ord_connected` set in a conditionally complete linear order is naturally a
+conditionally complete linear order. -/
+noncomputable instance ord_connected_subset_conditionally_complete_linear_order
+  [inhabited s] [ord_connected s] :
+  conditionally_complete_linear_order s :=
+subset_conditionally_complete_linear_order s Sup_within_of_ord_connected Inf_within_of_ord_connected
+
+end ord_connected
+
+end subtype

src/topology/algebra/ordered.lean

@@ -721,6 +721,55 @@ induced_order_topology' f @hf
   (λ a x xa, let ⟨b, xb, ba⟩ := H xa in ⟨b, hf.1 ba, le_of_lt xb⟩)
   (λ a x ax, let ⟨b, ab, bx⟩ := H ax in ⟨b, hf.1 ab, le_of_lt bx⟩)
 
+/-- On an `ord_connected` subset of a linear order, the order topology for the restriction of the
+order is the same as the restriction to the subset of the order topology. -/
+instance order_topology_of_ord_connected {α : Type u}
+  [ta : topological_space α] [decidable_linear_order α] [order_topology α]
+  {t : set α} [ht : ord_connected t] :
+  order_topology t :=
+begin
+  letI := induced (coe : t → α) ta,
+  refine ⟨eq_of_nhds_eq_nhds (λ a, _)⟩,
+  rw [nhds_induced, nhds_generate_from, nhds_eq_order (a : α)],
+  apply le_antisymm,
+  { refine le_infi (λ s, le_infi $ λ hs, le_principal_iff.2 _),
+    rcases hs with ⟨ab, b, rfl|rfl⟩,
+    { refine ⟨Ioi b, _, λ _, id⟩,
+      refine mem_inf_sets_of_left (mem_infi_sets b _),
+      exact mem_infi_sets ab (mem_principal_self (Ioi ↑b)) },
+    { refine ⟨Iio b, _, λ _, id⟩,
+      refine mem_inf_sets_of_right (mem_infi_sets b _),
+      exact mem_infi_sets ab (mem_principal_self (Iio b)) } },
+  { rw [← map_le_iff_le_comap],
+    refine le_inf _ _,
+    { refine le_infi (λ x, le_infi $ λ h, le_principal_iff.2 _),
+      by_cases hx : x ∈ t,
+      { refine mem_infi_sets (Ioi ⟨x, hx⟩) (mem_infi_sets ⟨h, ⟨⟨x, hx⟩, or.inl rfl⟩⟩ _),
+        exact λ _, id },
+      simp only [set_coe.exists, mem_set_of_eq, mem_map],
+      convert univ_sets _,
+      suffices hx' : ∀ (y : t), ↑y ∈ Ioi x,
+      { simp [hx'] },
+      intros y,
+      revert hx,
+      contrapose!,
+      -- here we use the `ord_connected` hypothesis
+      exact λ hx, ht y.2 a.2 ⟨le_of_not_gt hx, le_of_lt h⟩ },
+    { refine le_infi (λ x, le_infi $ λ h, le_principal_iff.2 _),
+      by_cases hx : x ∈ t,
+      { refine mem_infi_sets (Iio ⟨x, hx⟩) (mem_infi_sets ⟨h, ⟨⟨x, hx⟩, or.inr rfl⟩⟩ _),
+        exact λ _, id },
+      simp only [set_coe.exists, mem_set_of_eq, mem_map],
+      convert univ_sets _,
+      suffices hx' : ∀ (y : t), ↑y ∈ Iio x,
+      { simp [hx'] },
+      intros y,
+      revert hx,
+      contrapose!,
+      -- here we use the `ord_connected` hypothesis
+      exact λ hx, ht a.2 y.2 ⟨le_of_lt h, le_of_not_gt hx⟩ } }
+end
+
 lemma nhds_top_order [topological_space α] [order_top α] [order_topology α] :
   𝓝 (⊤:α) = (⨅l (h₂ : l < ⊤), 𝓟 (Ioi l)) :=
 by simp [nhds_eq_order (⊤:α)]