Skip to content

feat(Order/ConditionallyCompleteLattice): ConditionallyCompleteSemiLatticeInf #38192

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
Jun2M wants to merge 4 commits into
base: master
Choose a base branch
from
+109 −33
Draft

feat(Order/ConditionallyCompleteLattice): ConditionallyCompleteSemiLatticeInf #38192

Changes from 1 commit
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
3e97358
init
Jun2M Apr 17, 2026
a0a7539
uncomment
Jun2M Apr 18, 2026
022cd0d
name change
Jun2M Apr 18, 2026
9a10329
∀ ⦃x⦄, IsBot x -> sSup ∅ = x
Jun2M Apr 18, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
69 changes: 26 additions & 43 deletions Mathlib/Order/ConditionallyCompleteLattice/Defs.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -44,6 +44,8 @@ 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)
/-- If the lattice has a bottom element, then `sSup ∅` is the bottom element. -/
csSup_empty : ∀ ⦃x⦄, IsBot x -> sSup ∅ = x
Copy link
Copy Markdown
Collaborator

@vihdzp vihdzp Apr 19, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'd like to see this change done in a preliminary PR, which would also deprecate ConditionallyCompleteSemilatticeSupBot.

Copy link
Copy Markdown
Collaborator

@vihdzp vihdzp Apr 19, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I've opened a Zulip thread to double-check that this is a good idea.


/-- A conditionally complete semilattice is a semilattice in which every nonempty subset which is
bounded below has a greatest lower bound.
Expand All @@ -56,6 +58,8 @@ boundedness. -/
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)
/-- If the lattice has a top element, then `sInf ∅` is the top element. -/
csInf_empty : ∀ ⦃x⦄, IsTop x -> sInf ∅ = x

attribute [to_dual existing] ConditionallyCompleteSemilatticeInf.isGLB_csInf
ConditionallyCompleteSemilatticeInf.toSemilatticeInf
Expand All @@ -66,40 +70,16 @@ instance OrderDual.instConditionallyCompleteSemilatticeSup (α)
[h : ConditionallyCompleteSemilatticeInf α] : ConditionallyCompleteSemilatticeSup αᵒᵈ where
sSup := sInf (α := α)
isLUB_csSup := h.isGLB_csInf (α := α)
csSup_empty := h.csInf_empty (α := α)

@[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 existing]
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
theorem csSup_empty [ConditionallyCompleteSemilatticeSup α] {x : α} (h : IsBot x) : sSup ∅ = x :=
ConditionallyCompleteSemilatticeSup.csSup_empty h

/-- A conditionally complete lattice is a lattice in which
every nonempty subset which is bounded above has a supremum, and
Expand Down Expand Up @@ -153,15 +133,10 @@ hold in both worlds, sometimes with additional assumptions of nonemptiness or
boundedness. -/
class ConditionallyCompleteLinearOrderBot (α : Type*) extends ConditionallyCompleteLinearOrder α,
OrderBot α where
/-- The supremum of the empty set is special-cased to `⊥` -/
csSup_empty : sSup ∅ = ⊥

-- see Note [lower instance priority]
attribute [instance 100] ConditionallyCompleteLinearOrderBot.toOrderBot

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
Expand All @@ -173,12 +148,14 @@ constructor provides poor definitional equalities. If other fields are known ex
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)) :
(isGLB_sInf : ∀ s : Set α, BddBelow s → s.Nonempty → IsGLB s (sInf s))
(csInf_empty : ∀ ⦃x : α⦄, IsTop x -> sInf ∅ = x):
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
csInf_empty := csInf_empty

/-- Create a `ConditionallyCompleteSemilatticeInfBot` from a `PartialOrder`, `OrderBot` and `sInf`
function that returns the greatest lower bound of a nonempty set. Usually this constructor provides
Expand All @@ -190,13 +167,13 @@ poor definitional equalities. If other fields are known explicitly, they should
def conditionallyCompleteSemilatticeInfOfsInfTop (α : Type*) [PartialOrder α] [H1 : InfSet α]
[H2 : OrderTop α] (sInf_empty : sInf ∅ = (⊤ : α))
(isGLB_sInf : ∀ s : Set α, s.Nonempty → IsGLB s (sInf s)) :
ConditionallyCompleteSemilatticeInfTop α where
ConditionallyCompleteSemilatticeInf α where
__ := H1
__ := H2
__ := 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
csInf_empty _ hx := hx.eq_top ▸ 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
Expand Down Expand Up @@ -232,7 +209,8 @@ instance : ConditionallyCompleteLattice my_T :=
def conditionallyCompleteLatticeOfsSup (α : Type*) [H1 : PartialOrder α] [H2 : SupSet α]
(bddAbove_pair : ∀ a b : α, BddAbove ({a, b} : Set α))
(bddBelow_pair : ∀ a b : α, BddBelow ({a, b} : Set α))
(isLUB_sSup : ∀ s : Set α, BddAbove s → s.Nonempty → IsLUB s (sSup s)) :
(isLUB_sSup : ∀ s : Set α, BddAbove s → s.Nonempty → IsLUB s (sSup s))
(csSup_empty : ∀ ⦃x : α⦄, IsBot x -> sSup ∅ = x) :
ConditionallyCompleteLattice α where
__ := Lattice.ofIsLUBofIsGLB (fun a b ↦ sSup {a, b}) (fun a b ↦ sSup (lowerBounds {a, b}))
(fun a b ↦ isLUB_sSup {a, b} (bddAbove_pair a b) (insert_nonempty _ _))
Expand All @@ -242,6 +220,11 @@ def conditionallyCompleteLatticeOfsSup (α : Type*) [H1 : PartialOrder α] [H2 :
sInf s := sSup (lowerBounds s)
isLUB_csSup _ hn hb := isLUB_sSup _ hb hn
isGLB_csInf _ hn hb := isLUB_lowerBounds.mp (isLUB_sSup _ hn.bddAbove_lowerBounds hb)
csSup_empty := csSup_empty
csInf_empty x hx := by
rw [lowerBounds_empty]
exact isLUB_sSup univ ⟨x, fun ⦃a⦄ a_1 ↦ hx a⟩ ⟨x, mem_univ x⟩ |>.isLeast_iff_eq.mp
⟨fun ⦃a⦄ a_1 ↦ hx a, fun y hy ↦ hy <| mem_univ x⟩

/-- A version of `conditionallyCompleteLatticeOfsSup` when we already know that `α` is a lattice.

Expand All @@ -251,13 +234,13 @@ This should only be used when it is both hard and unnecessary to provide `sInf`

This should only be used when it is both hard and unnecessary to provide `sSup` explicitly. -/]
def conditionallyCompleteLatticeOfLatticeOfsSup (α : Type*) [H1 : Lattice α] [SupSet α]
(isLUB_sSup : ∀ s : Set α, BddAbove s → s.Nonempty → IsLUB s (sSup s)) :
ConditionallyCompleteLattice α :=
{ H1,
conditionallyCompleteLatticeOfsSup α
(fun a b => ⟨a ⊔ b, forall_insert_of_forall (forall_eq.mpr le_sup_right) le_sup_left⟩)
(fun a b => ⟨a ⊓ b, forall_insert_of_forall (forall_eq.mpr inf_le_right) inf_le_left⟩)
isLUB_sSup with }
(isLUB_sSup : ∀ s : Set α, BddAbove s → s.Nonempty → IsLUB s (sSup s))
(csSup_empty : ∀ ⦃x : α⦄, IsBot x -> sSup ∅ = x) : ConditionallyCompleteLattice α :=
{__ := H1,
__ := conditionallyCompleteLatticeOfsSup α
(fun a b => ⟨a ⊔ b, forall_insert_of_forall (forall_eq.mpr le_sup_right) le_sup_left⟩)
(fun a b => ⟨a ⊓ b, forall_insert_of_forall (forall_eq.mpr inf_le_right) inf_le_left⟩)
isLUB_sSup csSup_empty}

open scoped Classical in
/-- A well-founded linear order is conditionally complete, with a bottom element. -/
Expand Down
Loading