feat: basic API for ConditionallyCompletePartialOrder (#35047)

This develops the basic API for `ConditionallyCompletePartialOrder`. The API is copied from `ConditionallyCompleteLattice`, with `DirectedOn` assumptions added, and these lemmas are `protected` within that namespace. In a few cases, the lemmas were capable of being generalized outright, which we have done here.

As a result, some material moved out of `ConditionallyCompleteLattice/Basic` to `ConditionallyCompletePartialOrder/Basic`.

Author: j-loreaux

Mathlib.lean

@@ -5592,7 +5592,9 @@ public import Mathlib.Order.ConditionallyCompleteLattice.Defs
 public import Mathlib.Order.ConditionallyCompleteLattice.Finset
 public import Mathlib.Order.ConditionallyCompleteLattice.Group
 public import Mathlib.Order.ConditionallyCompleteLattice.Indexed
+public import Mathlib.Order.ConditionallyCompletePartialOrder.Basic
 public import Mathlib.Order.ConditionallyCompletePartialOrder.Defs
+public import Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
 public import Mathlib.Order.Copy
 public import Mathlib.Order.CountableDenseLinearOrder
 public import Mathlib.Order.Cover

Mathlib/Order/CompleteLattice/Basic.lean

@@ -225,7 +225,7 @@ protected theorem Equiv.iSup_congr {g : ι' → α} (e : ι ≃ ι') (h : ∀ x,
     ⨆ x, f x = ⨆ y, g y :=
   e.surjective.iSup_congr _ h
 
-@[congr]
+@[to_dual (attr := congr)]
 theorem iSup_congr_Prop {p q : Prop} {f₁ : p → α} {f₂ : q → α} (pq : p ↔ q)
     (f : ∀ x, f₁ (pq.mpr x) = f₂ x) : iSup f₁ = iSup f₂ := by
   obtain rfl := propext pq
@@ -241,6 +241,7 @@ theorem iSup_plift_down (f : ι → α) : ⨆ i, f (PLift.down i) = ⨆ i, f i :
 theorem iSup_range' (g : β → α) (f : ι → β) : ⨆ b : range f, g b = ⨆ i, g (f i) := by
   rw [iSup, iSup, ← image_eq_range, ← range_comp']
 
+@[to_dual]
 theorem sSup_image' {s : Set β} {f : β → α} : sSup (f '' s) = ⨆ a : s, f a := by
   rw [iSup, image_eq_range]
 
@@ -283,11 +284,6 @@ protected theorem Equiv.iInf_congr {g : ι' → α} (e : ι ≃ ι') (h : ∀ x,
     ⨅ x, f x = ⨅ y, g y :=
   @Equiv.iSup_congr αᵒᵈ _ _ _ _ _ e h
 
-@[congr]
-theorem iInf_congr_Prop {p q : Prop} {f₁ : p → α} {f₂ : q → α} (pq : p ↔ q)
-    (f : ∀ x, f₁ (pq.mpr x) = f₂ x) : iInf f₁ = iInf f₂ :=
-  @iSup_congr_Prop αᵒᵈ _ p q f₁ f₂ pq f
-
 theorem iInf_plift_up (f : PLift ι → α) : ⨅ i, f (PLift.up i) = ⨅ i, f i :=
   (PLift.up_surjective.iInf_congr _) fun _ => rfl
 
@@ -297,9 +293,6 @@ theorem iInf_plift_down (f : ι → α) : ⨅ i, f (PLift.down i) = ⨅ i, f i :
 theorem iInf_range' (g : β → α) (f : ι → β) : ⨅ b : range f, g b = ⨅ i, g (f i) :=
   @iSup_range' αᵒᵈ _ _ _ _ _
 
-theorem sInf_image' {s : Set β} {f : β → α} : sInf (f '' s) = ⨅ a : s, f a :=
-  @sSup_image' αᵒᵈ _ _ _ _
-
 end InfSet
 
 section
@@ -1034,13 +1027,10 @@ end le
 ### `iSup` and `iInf` under `Type`
 -/
 
-
+@[to_dual iInf_of_isEmpty]
 theorem iSup_of_empty' {α ι} [SupSet α] [IsEmpty ι] (f : ι → α) : iSup f = sSup (∅ : Set α) :=
   congr_arg sSup (range_eq_empty f)
 
-theorem iInf_of_isEmpty {α ι} [InfSet α] [IsEmpty ι] (f : ι → α) : iInf f = sInf (∅ : Set α) :=
-  congr_arg sInf (range_eq_empty f)
-
 theorem iSup_of_empty [IsEmpty ι] (f : ι → α) : iSup f = ⊥ :=
   (iSup_of_empty' f).trans sSup_empty
 

Mathlib/Order/CompletePartialOrder.lean

@@ -6,6 +6,7 @@ Authors: Christopher Hoskin
 module
 
 public import Mathlib.Order.OmegaCompletePartialOrder
+public import Mathlib.Order.ConditionallyCompletePartialOrder.Defs
 
 /-!
 # Complete Partial Orders
@@ -75,14 +76,20 @@ lemma CompletePartialOrder.scottContinuous {f : α → β} :
 open OmegaCompletePartialOrder
 
 /-- A complete partial order is an ω-complete partial order. -/
-instance CompletePartialOrder.toOmegaCompletePartialOrder : OmegaCompletePartialOrder α where
+instance (priority := 100) CompletePartialOrder.toOmegaCompletePartialOrder :
+    OmegaCompletePartialOrder α where
   ωSup c := ⨆ n, c n
   le_ωSup c := c.directed.le_iSup
   ωSup_le c _ := c.directed.iSup_le
 
+/-- A complete partial order is an conditionally complete partial order. -/
+instance (priority := 100) [CompletePartialOrder α] : ConditionallyCompletePartialOrderSup α where
+  isLUB_csSup_of_directed _ h_dir _ _ := h_dir.isLUB_sSup
+
 end CompletePartialOrder
 
 /-- A complete lattice is a complete partial order. -/
-instance CompleteLattice.toCompletePartialOrder [CompleteLattice α] : CompletePartialOrder α where
+instance (priority := 100) CompleteLattice.toCompletePartialOrder [CompleteLattice α] :
+    CompletePartialOrder α where
   sSup := sSup
   lubOfDirected _ _ := isLUB_sSup _

Mathlib/Order/ConditionallyCompleteLattice/Basic.lean

@@ -7,6 +7,7 @@ module
 
 public import Mathlib.Data.Set.Lattice
 public import Mathlib.Order.ConditionallyCompleteLattice.Defs
+public import Mathlib.Order.ConditionallyCompletePartialOrder.Basic
 
 /-!
 # Theory of conditionally complete lattices
@@ -224,22 +225,13 @@ theorem isGLB_csInf (ne : s.Nonempty) (H : BddBelow s) : IsGLB s (sInf s) :=
 theorem IsLUB.csSup_eq (H : IsLUB s a) (ne : s.Nonempty) : sSup s = a :=
   (isLUB_csSup ne ⟨a, H.1⟩).unique H
 
-/-- A greatest element of a set is the supremum of this set. -/
-theorem IsGreatest.csSup_eq (H : IsGreatest s a) : sSup s = a :=
-  H.isLUB.csSup_eq H.nonempty
-
-theorem IsGreatest.csSup_mem (H : IsGreatest s a) : sSup s ∈ s :=
-  H.csSup_eq.symm ▸ H.1
-
 theorem IsGLB.csInf_eq (H : IsGLB s a) (ne : s.Nonempty) : sInf s = a :=
   (isGLB_csInf ne ⟨a, H.1⟩).unique H
 
-/-- A least element of a set is the infimum of this set. -/
-theorem IsLeast.csInf_eq (H : IsLeast s a) : sInf s = a :=
-  H.isGLB.csInf_eq H.nonempty
-
-theorem IsLeast.csInf_mem (H : IsLeast s a) : sInf s ∈ s :=
-  H.csInf_eq.symm ▸ H.1
+instance (priority := 100) ConditionallyCompleteLattice.toConditionallyCompletePartialOrder :
+    ConditionallyCompletePartialOrder α where
+  isGLB_csInf_of_directed _ _ non bdd := isGLB_csInf non bdd
+  isLUB_csSup_of_directed _ _ non bdd := isLUB_csSup non bdd
 
 theorem subset_Icc_csInf_csSup (hb : BddBelow s) (ha : BddAbove s) : s ⊆ Icc (sInf s) (sSup s) :=
   fun _ hx => ⟨csInf_le hb hx, le_csSup ha hx⟩
@@ -310,16 +302,6 @@ theorem exists_between_of_forall_le (sne : s.Nonempty) (tne : t.Nonempty)
     (hst : ∀ x ∈ s, ∀ y ∈ t, x ≤ y) : (upperBounds s ∩ lowerBounds t).Nonempty :=
   ⟨sInf t, fun x hx => le_csInf tne <| hst x hx, fun _ hy => csInf_le (sne.mono hst) hy⟩
 
-/-- The supremum of a singleton is the element of the singleton -/
-@[simp]
-theorem csSup_singleton (a : α) : sSup {a} = a :=
-  isGreatest_singleton.csSup_eq
-
-/-- The infimum of a singleton is the element of the singleton -/
-@[simp]
-theorem csInf_singleton (a : α) : sInf {a} = a :=
-  isLeast_singleton.csInf_eq
-
 theorem csSup_pair (a b : α) : sSup {a, b} = a ⊔ b :=
   (@isLUB_pair _ _ a b).csSup_eq (insert_nonempty _ _)
 
@@ -367,18 +349,6 @@ nonempty and bounded below. -/
 theorem csInf_insert (hs : BddBelow s) (sne : s.Nonempty) : sInf (insert a s) = a ⊓ sInf s :=
   csSup_insert (α := αᵒᵈ) hs sne
 
-@[simp]
-theorem csInf_Icc (h : a ≤ b) : sInf (Icc a b) = a :=
-  (isGLB_Icc h).csInf_eq (nonempty_Icc.2 h)
-
-@[simp]
-theorem csInf_Ici : sInf (Ici a) = a :=
-  isLeast_Ici.csInf_eq
-
-@[simp]
-theorem csInf_Ico (h : a < b) : sInf (Ico a b) = a :=
-  (isGLB_Ico h).csInf_eq (nonempty_Ico.2 h)
-
 @[simp]
 theorem csInf_Ioc [DenselyOrdered α] (h : a < b) : sInf (Ioc a b) = a :=
   (isGLB_Ioc h).csInf_eq (nonempty_Ioc.2 h)
@@ -392,27 +362,15 @@ theorem csInf_Ioi [NoMaxOrder α] [DenselyOrdered α] : sInf (Ioi a) = a :=
 theorem csInf_Ioo [DenselyOrdered α] (h : a < b) : sInf (Ioo a b) = a :=
   (isGLB_Ioo h).csInf_eq (nonempty_Ioo.2 h)
 
-@[simp]
-theorem csSup_Icc (h : a ≤ b) : sSup (Icc a b) = b :=
-  (isLUB_Icc h).csSup_eq (nonempty_Icc.2 h)
-
 @[simp]
 theorem csSup_Ico [DenselyOrdered α] (h : a < b) : sSup (Ico a b) = b :=
   (isLUB_Ico h).csSup_eq (nonempty_Ico.2 h)
 
-@[simp]
-theorem csSup_Iic : sSup (Iic a) = a :=
-  isGreatest_Iic.csSup_eq
-
 @[simp]
 theorem csSup_Iio [NoMinOrder α] [DenselyOrdered α] : sSup (Iio a) = a :=
   csSup_eq_of_forall_le_of_forall_lt_exists_gt nonempty_Iio (fun _ => le_of_lt) fun w hw => by
     simpa [and_comm] using exists_between hw
 
-@[simp]
-theorem csSup_Ioc (h : a < b) : sSup (Ioc a b) = b :=
-  (isLUB_Ioc h).csSup_eq (nonempty_Ioc.2 h)
-
 @[simp]
 theorem csSup_Ioo [DenselyOrdered α] (h : a < b) : sSup (Ioo a b) = b :=
   (isLUB_Ioo h).csSup_eq (nonempty_Ioo.2 h)
@@ -424,12 +382,6 @@ theorem csSup_eq_of_is_forall_le_of_forall_le_imp_ge (hs : s.Nonempty) (h_is_ub
     (h_b_le_ub : ∀ ub, (∀ a ∈ s, a ≤ ub) → b ≤ ub) : sSup s = b :=
   (csSup_le hs h_is_ub).antisymm ((h_b_le_ub _) fun _ => le_csSup ⟨b, h_is_ub⟩)
 
-lemma sup_eq_top_of_top_mem [OrderTop α] (h : ⊤ ∈ s) : sSup s = ⊤ :=
-  top_unique <| le_csSup (OrderTop.bddAbove s) h
-
-lemma inf_eq_bot_of_bot_mem [OrderBot α] (h : ⊥ ∈ s) : sInf s = ⊥ :=
-  bot_unique <| csInf_le (OrderBot.bddBelow s) h
-
 end ConditionallyCompleteLattice
 
 instance Pi.conditionallyCompleteLattice {ι : Type*} {α : ι → Type*}

Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean

@@ -6,6 +6,7 @@ Authors: Sébastian Gouëzel
 module
 
 public import Mathlib.Order.ConditionallyCompleteLattice.Basic
+public import Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
 
 /-!
 # Indexed sup / inf in conditionally complete lattices
@@ -181,68 +182,6 @@ lemma ciInf_le_ciSup [Nonempty ι] {f : ι → α} (hf : BddBelow (range f)) (hf
     ⨅ i, f i ≤ ⨆ i, f i :=
   (ciInf_le hf (Classical.arbitrary _)).trans <| le_ciSup hf' (Classical.arbitrary _)
 
-@[simp]
-theorem ciSup_const [hι : Nonempty ι] {a : α} : ⨆ _ : ι, a = a := by
-  rw [iSup, range_const, csSup_singleton]
-
-@[simp]
-theorem ciInf_const [Nonempty ι] {a : α} : ⨅ _ : ι, a = a :=
-  ciSup_const (α := αᵒᵈ)
-
-@[simp]
-theorem ciSup_unique [Unique ι] {s : ι → α} : ⨆ i, s i = s default := by
-  have : ∀ i, s i = s default := fun i => congr_arg s (Unique.eq_default i)
-  simp only [this, ciSup_const]
-
-@[simp]
-theorem ciInf_unique [Unique ι] {s : ι → α} : ⨅ i, s i = s default :=
-  ciSup_unique (α := αᵒᵈ)
-
-theorem ciSup_subsingleton [Subsingleton ι] (i : ι) (s : ι → α) : ⨆ i, s i = s i :=
-  @ciSup_unique α ι _ ⟨⟨i⟩, fun j => Subsingleton.elim j i⟩ _
-
-theorem ciInf_subsingleton [Subsingleton ι] (i : ι) (s : ι → α) : ⨅ i, s i = s i :=
-  @ciInf_unique α ι _ ⟨⟨i⟩, fun j => Subsingleton.elim j i⟩ _
-
-theorem ciSup_pos {p : Prop} {f : p → α} (hp : p) : ⨆ h : p, f h = f hp := by
-  simp [hp]
-
-theorem ciInf_pos {p : Prop} {f : p → α} (hp : p) : ⨅ h : p, f h = f hp := by
-  simp [hp]
-
-lemma ciSup_neg {p : Prop} {f : p → α} (hp : ¬ p) :
-    ⨆ (h : p), f h = sSup (∅ : Set α) := by
-  rw [iSup]
-  congr
-  rwa [range_eq_empty_iff, isEmpty_Prop]
-
-lemma ciInf_neg {p : Prop} {f : p → α} (hp : ¬ p) :
-    ⨅ (h : p), f h = sInf (∅ : Set α) :=
-  ciSup_neg (α := αᵒᵈ) hp
-
-lemma ciSup_eq_ite {p : Prop} [Decidable p] {f : p → α} :
-    (⨆ h : p, f h) = if h : p then f h else sSup (∅ : Set α) := by
-  by_cases H : p <;> simp [ciSup_neg, H]
-
-lemma ciInf_eq_ite {p : Prop} [Decidable p] {f : p → α} :
-    (⨅ h : p, f h) = if h : p then f h else sInf (∅ : Set α) :=
-  ciSup_eq_ite (α := αᵒᵈ)
-
-theorem cbiSup_eq_of_forall {p : ι → Prop} {f : Subtype p → α} (hp : ∀ i, p i) :
-    ⨆ (i) (h : p i), f ⟨i, h⟩ = iSup f := by
-  simp only [hp, ciSup_unique]
-  simp only [iSup]
-  congr
-  apply Subset.antisymm
-  · rintro - ⟨i, rfl⟩
-    simp
-  · rintro - ⟨i, rfl⟩
-    simp
-
-theorem cbiInf_eq_of_forall {p : ι → Prop} {f : Subtype p → α} (hp : ∀ i, p i) :
-    ⨅ (i) (h : p i), f ⟨i, h⟩ = iInf f :=
-  cbiSup_eq_of_forall (α := αᵒᵈ) hp
-
 /-- Introduction rule to prove that `b` is the supremum of `f`: it suffices to check that `b`
 is larger than `f i` for all `i`, and that this is not the case of any `w<b`.
 See `iSup_eq_of_forall_le_of_forall_lt_exists_gt` for a version in complete lattices. -/
@@ -258,24 +197,6 @@ theorem ciInf_eq_of_forall_ge_of_forall_gt_exists_lt [Nonempty ι] {f : ι → 
     (h₂ : ∀ w, b < w → ∃ i, f i < w) : ⨅ i : ι, f i = b :=
   ciSup_eq_of_forall_le_of_forall_lt_exists_gt (α := αᵒᵈ) h₁ h₂
 
-/-- **Nested intervals lemma**: if `f` is a monotone sequence, `g` is an antitone sequence, and
-`f n ≤ g n` for all `n`, then `⨆ n, f n` belongs to all the intervals `[f n, g n]`. -/
-theorem Monotone.ciSup_mem_iInter_Icc_of_antitone [SemilatticeSup β] {f g : β → α} (hf : Monotone f)
-    (hg : Antitone g) (h : f ≤ g) : (⨆ n, f n) ∈ ⋂ n, Icc (f n) (g n) := by
-  refine mem_iInter.2 fun n => ?_
-  haveI : Nonempty β := ⟨n⟩
-  have : ∀ m, f m ≤ g n := fun m => hf.forall_le_of_antitone hg h m n
-  exact ⟨le_ciSup ⟨g <| n, forall_mem_range.2 this⟩ _, ciSup_le this⟩
-
-/-- Nested intervals lemma: if `[f n, g n]` is an antitone sequence of nonempty
-closed intervals, then `⨆ n, f n` belongs to all the intervals `[f n, g n]`. -/
-theorem ciSup_mem_iInter_Icc_of_antitone_Icc [SemilatticeSup β] {f g : β → α}
-    (h : Antitone fun n => Icc (f n) (g n)) (h' : ∀ n, f n ≤ g n) :
-    (⨆ n, f n) ∈ ⋂ n, Icc (f n) (g n) :=
-  Monotone.ciSup_mem_iInter_Icc_of_antitone
-    (fun _ n hmn => ((Icc_subset_Icc_iff (h' n)).1 (h hmn)).1)
-    (fun _ n hmn => ((Icc_subset_Icc_iff (h' n)).1 (h hmn)).2) h'
-
 lemma Set.Iic_ciInf [Nonempty ι] {f : ι → α} (hf : BddBelow (range f)) :
     Iic (⨅ i, f i) = ⋂ i, Iic (f i) := by
   ext
@@ -285,22 +206,6 @@ lemma Set.Ici_ciSup [Nonempty ι] {f : ι → α} (hf : BddAbove (range f)) :
     Ici (⨆ i, f i) = ⋂ i, Ici (f i) :=
   Iic_ciInf (α := αᵒᵈ) hf
 
-theorem ciSup_Iic [Preorder β] {f : β → α} (a : β) (hf : Monotone f) :
-    ⨆ x : Iic a, f x = f a := by
-  have H : BddAbove (range fun x : Iic a ↦ f x) := ⟨f a, fun _ ↦ by aesop⟩
-  apply (le_ciSup H (⟨a, le_refl a⟩ : Iic a)).antisymm'
-  rw [ciSup_le_iff H]
-  rintro ⟨a, h⟩
-  exact hf h
-
-theorem ciInf_Ici [Preorder β] {f : β → α} (a : β) (hf : Monotone f) :
-    ⨅ x : Ici a, f x = f a := by
-  have H : BddBelow (range fun x : Ici a ↦ f x) := ⟨f a, fun _ ↦ by aesop⟩
-  apply (ciInf_le H (⟨a, le_refl a⟩ : Ici a)).antisymm
-  rw [le_ciInf_iff H]
-  rintro ⟨a, h⟩
-  exact hf h
-
 theorem ciSup_subtype [Nonempty ι] {p : ι → Prop} [Nonempty (Subtype p)] {f : Subtype p → α}
     (hf : BddAbove (Set.range f)) (hf' : sSup ∅ ≤ iSup f) :
     iSup f = ⨆ (i) (h : p i), f ⟨i, h⟩ := by