feat(Order/ConditionallyCompleteLattice): ConditionallyCompleteSemiLatticeInf

Mathlib/Order/ConditionallyCompleteLattice/Basic.lean

@@ -163,8 +163,8 @@ namespace OrderDual
 
 instance instConditionallyCompleteLattice (α : Type*) [ConditionallyCompleteLattice α] :
     ConditionallyCompleteLattice αᵒᵈ where
-  isLUB_csSup := ConditionallyCompleteLattice.isGLB_csInf (α := α)
-  isGLB_csInf := ConditionallyCompleteLattice.isLUB_csSup (α := α)
+  isLUB_csSup _ hn hb := isGLB_csInf (α := α) hn hb
+  isGLB_csInf _ hn hb := isLUB_csSup (α := α) hn hb
 
 instance (α : Type*) [ConditionallyCompleteLinearOrder α] :
     ConditionallyCompleteLinearOrder αᵒᵈ where
@@ -179,10 +179,6 @@ section ConditionallyCompleteLattice
 
 variable [ConditionallyCompleteLattice α] {s t : Set α} {a b : α}
 
-@[to_dual]
-theorem isLUB_csSup (hn : s.Nonempty) (hb : BddAbove s := by bddDefault) : IsLUB s (sSup s) :=
-  ConditionallyCompleteLattice.isLUB_csSup _ hn hb
-
 theorem le_csSup (h₁ : BddAbove s) (h₂ : a ∈ s) : a ≤ sSup s :=
   (isLUB_csSup (nonempty_of_mem h₂) h₁).1 h₂
 
@@ -223,7 +219,7 @@ theorem IsLUB.csSup_eq (H : IsLUB s a) (ne : s.Nonempty) : sSup s = a :=
 instance (priority := 100) ConditionallyCompleteLattice.toConditionallyCompletePartialOrder :
     ConditionallyCompletePartialOrder α where
   isGLB_csInf_of_directed _ _ := isGLB_csInf _
-  isLUB_csSup_of_directed _ _ := isLUB_csSup _
+  isLUB_csSup_of_directed _ _ hn hb := isLUB_csSup (α := α) hn hb
 
 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⟩
@@ -544,10 +540,6 @@ theorem csInf_univ [ConditionallyCompleteLattice α] [OrderBot α] : sInf (univ
 
 variable [ConditionallyCompleteLinearOrderBot α] {s : Set α} {a : α}
 
-@[simp]
-theorem csSup_empty : (sSup ∅ : α) = ⊥ :=
-  ConditionallyCompleteLinearOrderBot.csSup_empty
-
 theorem isLUB_csSup' {s : Set α} (hs : BddAbove s) : IsLUB s (sSup s) := by
   rcases eq_empty_or_nonempty s with (rfl | hne)
   · simp only [csSup_empty, isLUB_empty]

Mathlib/Order/ConditionallyCompleteLattice/Defs.lean

@@ -34,6 +34,73 @@ open Set
 
 variable {α β γ : Type*} {ι : Sort*}
 
+/-- A conditionally complete semilattice is a semilattice in which every nonempty subset which is
+  bounded above has a least upper bound.
+
+To differentiate the statements from the corresponding statements in (unconditional)
+complete lattices, we prefix `sSup` by a `c` everywhere. The same statements should
+hold in both worlds, sometimes with additional assumptions of nonemptiness or
+boundedness. -/
+class ConditionallyCompleteSemiLatticeSup (α : Type*) extends SemilatticeSup α, SupSet α where
+  /-- Every nonempty subset which is bounded above has a least upper bound. -/
+  isLUB_csSup : ∀ s : Set α, s.Nonempty → BddAbove s → IsLUB s (sSup s)
+
+/-- A conditionally complete semilattice is a semilattice in which every nonempty subset which is
+bounded below has a greatest lower bound.
+
+To differentiate the statements from the corresponding statements in (unconditional)
+complete lattices, we prefix `sInf` by a `c` everywhere. The same statements should
+hold in both worlds, sometimes with additional assumptions of nonemptiness or
+boundedness. -/
+@[to_dual]
+class ConditionallyCompleteSemiLatticeInf (α : Type*) extends SemilatticeInf α, InfSet α where
+  /-- Every nonempty subset which is bounded below has a greatest lower bound. -/
+  isGLB_csInf : ∀ s : Set α, s.Nonempty → BddBelow s → IsGLB s (sInf s)
+
+attribute [to_dual existing] ConditionallyCompleteSemiLatticeInf.isGLB_csInf
+  ConditionallyCompleteSemiLatticeInf.toSemilatticeInf
+  ConditionallyCompleteSemiLatticeInf.toInfSet
+
+@[to_dual]
+instance OrderDual.instConditionallyCompleteSemiLatticeSup (α)
+    [h : ConditionallyCompleteSemiLatticeInf α] : ConditionallyCompleteSemiLatticeSup αᵒᵈ where
+  sSup := sInf (α := α)
+  isLUB_csSup := h.isGLB_csInf (α := α)
+
+@[to_dual]
+theorem isGLB_csInf [ConditionallyCompleteSemiLatticeInf α] {s : Set α} (hn : s.Nonempty)
+    (hb : BddBelow s := by bddDefault) : IsGLB s (sInf s) :=
+  ConditionallyCompleteSemiLatticeInf.isGLB_csInf s hn hb
+
+/-- A conditionally complete semilattice with `Top` is a semilattice with greatest element, in which
+  every nonempty subset (necessarily bounded above) has a supremum.
+
+To differentiate the statements from the corresponding statements in (unconditional)
+complete lattices, we prefix `sSup` by a `c` everywhere. The same statements should
+hold in both worlds, sometimes with additional assumptions of nonemptiness or
+boundedness. -/
+class ConditionallyCompleteSemiLatticeSupBot (α : Type*) extends
+  ConditionallyCompleteSemiLatticeSup α, OrderBot α where
+  /-- The supremum of the empty set is `⊥`. -/
+  csSup_empty : sSup ∅ = (⊥ : α)
+
+/-- A conditionally complete semilattice with `Bot` is a semilattice with least element, in which
+  every nonempty subset (necessarily bounded below) has an infimum.
+
+To differentiate the statements from the corresponding statements in (unconditional)
+complete lattices, we prefix `sInf` by a `c` everywhere. The same statements should
+hold in both worlds, sometimes with additional assumptions of nonemptiness or
+boundedness. -/
+@[to_dual]
+class ConditionallyCompleteSemiLatticeInfTop (α : Type*) extends
+  ConditionallyCompleteSemiLatticeInf α, OrderTop α where
+  /-- The infimum of the empty set is `⊥`. -/
+  csInf_empty : sInf ∅ = (⊤ : α)
+
+@[to_dual, simp]
+theorem csSup_empty [ConditionallyCompleteSemiLatticeSupBot α] : sSup ∅ = (⊥ : α) :=
+  ConditionallyCompleteSemiLatticeSupBot.csSup_empty
+
 /-- A conditionally complete lattice is a lattice in which
 every nonempty subset which is bounded above has a supremum, and
 every nonempty subset which is bounded below has an infimum.
@@ -43,15 +110,10 @@ To differentiate the statements from the corresponding statements in (unconditio
 complete lattices, we prefix `sInf` and `sSup` by a `c` everywhere. The same statements should
 hold in both worlds, sometimes with additional assumptions of nonemptiness or
 boundedness. -/
-class ConditionallyCompleteLattice (α : Type*) extends Lattice α, SupSet α, InfSet α where
-  /-- Every nonempty subset which is bounded above has a least upper bound. -/
-  isLUB_csSup : ∀ s : Set α, s.Nonempty → BddAbove s → IsLUB s (sSup s)
-  /-- Every nonempty subset which is bounded below has a greatest lower bound. -/
-  isGLB_csInf : ∀ s : Set α, s.Nonempty → BddBelow s → IsGLB s (sInf s)
+class ConditionallyCompleteLattice (α : Type*) extends
+  ConditionallyCompleteSemiLatticeSup α, ConditionallyCompleteSemiLatticeInf α
 
-attribute [to_dual self (reorder := 3 4, 5 6)] ConditionallyCompleteLattice.mk
-attribute [to_dual existing] ConditionallyCompleteLattice.toSupSet
-attribute [to_dual existing] ConditionallyCompleteLattice.isLUB_csSup
+attribute [to_dual existing] ConditionallyCompleteLattice.toConditionallyCompleteSemiLatticeInf
 
 /-- A conditionally complete linear order is a linear order in which
 every nonempty subset which is bounded above has a supremum, and
@@ -97,7 +159,46 @@ class ConditionallyCompleteLinearOrderBot (α : Type*) extends ConditionallyComp
 -- see Note [lower instance priority]
 attribute [instance 100] ConditionallyCompleteLinearOrderBot.toOrderBot
 
-/-- Create a `ConditionallyCompleteLattice` from a `PartialOrder` and `sup` function
+instance [ConditionallyCompleteLinearOrderBot α] : ConditionallyCompleteSemiLatticeSupBot α where
+  csSup_empty := ConditionallyCompleteLinearOrderBot.csSup_empty
+
+/-- Create a `ConditionallyCompleteSemiLatticeInf` from a `PartialOrder` and `sInf` function
+that returns the greatest lower bound of a nonempty set which is bounded below. Usually this
+constructor provides poor definitional equalities.  If other fields are known explicitly, they
+should be provided. -/
+@[to_dual (attr := implicit_reducible)
+/-- Create a `ConditionallyCompleteSemiLatticeSup` from a `PartialOrder` and `sSup` function
+that returns the least upper bound of a nonempty set which is bounded above. Usually this
+constructor provides poor definitional equalities.  If other fields are known explicitly, they
+should be provided. -/]
+def conditionallyCompleteSemiLatticeInfOfsInf (α : Type*) [H1 : PartialOrder α] [H2 : InfSet α]
+    (bddBelow_pair : ∀ a b : α, BddBelow ({a, b} : Set α))
+    (isGLB_sInf : ∀ s : Set α, BddBelow s → s.Nonempty → IsGLB s (sInf s)) :
+    ConditionallyCompleteSemiLatticeInf α where
+  __ := H2
+  __ := SemilatticeInf.ofIsGLB (fun a b ↦ sInf {a, b})
+    (fun a b ↦ isGLB_sInf {a, b} (bddBelow_pair a b) (insert_nonempty _ _))
+  isGLB_csInf _ hn hb := isGLB_sInf _ hb hn
+
+/-- Create a `ConditionallyCompleteSemiLatticeInfBot` from a `PartialOrder`, `OrderBot` and `sInf`
+function that returns the greatest lower bound of a nonempty set. Usually this constructor provides
+poor definitional equalities.  If other fields are known explicitly, they should be provided. -/
+@[to_dual (attr := implicit_reducible)
+/-- Create a `ConditionallyCompleteSemiLatticeSupTop` from a `PartialOrder`, `OrderTop` and `sSup`
+function that returns the least upper bound of a nonempty set. Usually this constructor provides
+poor definitional equalities.  If other fields are known explicitly, they should be provided. -/]
+def conditionallyCompleteSemiLatticeInfOfsInfTop (α : Type*) [H1 : PartialOrder α] [H2 : InfSet α]
+    [H3 : OrderTop α] (sInf_empty : sInf ∅ = (⊤ : α))
+    (isGLB_sInf : ∀ s : Set α, s.Nonempty → IsGLB s (sInf s)) :
+    ConditionallyCompleteSemiLatticeInfTop α where
+  __ := H2
+  __ := H3
+  __ := SemilatticeInf.ofIsGLB (fun a b ↦ sInf {a, b})
+    (fun a b ↦ isGLB_sInf {a, b} (insert_nonempty _ _))
+  isGLB_csInf _ hn _ := isGLB_sInf _ hn
+  csInf_empty := sInf_empty
+
+/-- Create a `ConditionallyCompleteLattice` from a `PartialOrder` and `sSup` function
 that returns the least upper bound of a nonempty set which is bounded above. Usually this
 constructor provides poor definitional equalities.  If other fields are known explicitly, they
 should be provided; for example, if `inf` is known explicitly, construct the
@@ -112,7 +213,7 @@ instance : ConditionallyCompleteLattice my_T where
   __ := conditionallyCompleteLatticeOfsSup my_T ...
 ```
 -/
-@[to_dual (attr := implicit_reducible) (reorder := 4 5)
+@[to_dual (attr := implicit_reducible) (reorder := H1 H2)
 /-- Create a `ConditionallyCompleteLattice` from a `PartialOrder` and `sInf` function
 that returns the greatest lower bound of a nonempty set which is bounded below. Usually this
 constructor provides poor definitional equalities.  If other fields are known explicitly, they

Mathlib/Order/Copy.lean

@@ -259,8 +259,8 @@ def ConditionallyCompleteLattice.copy (c : ConditionallyCompleteLattice α)
     (sSup : Set α → α) (eq_sSup : sSup = (by infer_instance : SupSet α).sSup)
     (sInf : Set α → α) (eq_sInf : sInf = (by infer_instance : InfSet α).sInf) :
     ConditionallyCompleteLattice α where
-  toLattice := Lattice.copy (@ConditionallyCompleteLattice.toLattice α c)
-    le eq_le sup eq_sup inf eq_inf
+  -- toLattice := Lattice.copy (@ConditionallyCompleteLattice.toLattice α c)
+  --   le eq_le sup eq_sup inf eq_inf
   sSup := sSup
   sInf := sInf
   isLUB_csSup := by subst_vars; exact c.isLUB_csSup