[Merged by Bors] - feat: define ConditionallyCompletePartialOrder#35046
Closed
j-loreaux wants to merge 2 commits intoleanprover-community:masterfrom
Closed
[Merged by Bors] - feat: define ConditionallyCompletePartialOrder#35046j-loreaux wants to merge 2 commits intoleanprover-community:masterfrom
ConditionallyCompletePartialOrder#35046j-loreaux wants to merge 2 commits intoleanprover-community:masterfrom
Conversation
PR summary 668a53718fImport changes for modified filesNo significant changes to the import graph Import changes for all files
|
b-mehta
reviewed
Feb 9, 2026
Contributor
b-mehta
left a comment
b-mehta
left a comment
There was a problem hiding this comment.
Can we also have the instance that every ConditionallyCompletePartialOrderSup is a CompletePartialOrder?
1 task
Contributor
Author
b-mehta
approved these changes
Feb 10, 2026
mathlib-bors bot
pushed a commit
that referenced
this pull request
Feb 12, 2026
This file defines *conditionally complete partial orders* with suprema, infima or both. These are partial orders where every nonempty, upwards (downwards) directed set which is bounded above (below) has a least upper bound (greatest lower bound). This class extends `SupSet` (`InfSet`) and the requirement is that `sSup` (`sInf`) must be the least upper bound.
The three classes defined herein are:
+ `ConditionallyCompletePartialOrderSup` for partial orders with suprema,
+ `ConditionallyCompletePartialOrderInf` for partial orders with infima, and
+ `ConditionallyCompletePartialOrder` for partial orders with both suprema and infima
One common use case for these classes is the order on a von Neumann algebra, or W⋆-algebra. This is the strongest order-theoretic structure satisfied by a von Neumann algebra; in particular it is *not* a conditionally complete *lattice*, and indeed it is a lattice if and only if the algebra is commutative. In addition, `ℂ` can be made to satisfy this class (one must provide a suitable `SupSet` instance), with the order `w ≤ z ↔ w.re ≤ z.re ∧ w.im = z.im`, which is available in the `ComplexOrder` namespace.
These use cases are the motivation for defining three classes, as compared with other parts of the order theory library, where only the supremum versions are defined (e.g., `CompletePartialOrder` and `OmegaCompletePartialOrder`). We note that, if these classes are used outside of order theory, then it is more likely that the infimum versions would be useful. Indeed, whenever the underlying type has an antitone involution (e.g., if it is an ordered ring, then negation would be such a map), then any `ConditionallyCompletePartialOrder{Sup,Inf}` is automatically a `ConditionallyCompletePartialOrder`. Because of the `to_dual` attribute, the additional overhead required to add and maintain the infimum version is minimal.
Contributor
|
Pull request successfully merged into master. Build succeeded:
|
mathlib-bors
bot
changed the title
ConditionallyCompletePartialOrderConditionallyCompletePartialOrder
kim-em
pushed a commit
to kim-em/mathlib4
that referenced
this pull request
Feb 14, 2026
…y#35046) This file defines *conditionally complete partial orders* with suprema, infima or both. These are partial orders where every nonempty, upwards (downwards) directed set which is bounded above (below) has a least upper bound (greatest lower bound). This class extends `SupSet` (`InfSet`) and the requirement is that `sSup` (`sInf`) must be the least upper bound. The three classes defined herein are: + `ConditionallyCompletePartialOrderSup` for partial orders with suprema, + `ConditionallyCompletePartialOrderInf` for partial orders with infima, and + `ConditionallyCompletePartialOrder` for partial orders with both suprema and infima One common use case for these classes is the order on a von Neumann algebra, or W⋆-algebra. This is the strongest order-theoretic structure satisfied by a von Neumann algebra; in particular it is *not* a conditionally complete *lattice*, and indeed it is a lattice if and only if the algebra is commutative. In addition, `ℂ` can be made to satisfy this class (one must provide a suitable `SupSet` instance), with the order `w ≤ z ↔ w.re ≤ z.re ∧ w.im = z.im`, which is available in the `ComplexOrder` namespace. These use cases are the motivation for defining three classes, as compared with other parts of the order theory library, where only the supremum versions are defined (e.g., `CompletePartialOrder` and `OmegaCompletePartialOrder`). We note that, if these classes are used outside of order theory, then it is more likely that the infimum versions would be useful. Indeed, whenever the underlying type has an antitone involution (e.g., if it is an ordered ring, then negation would be such a map), then any `ConditionallyCompletePartialOrder{Sup,Inf}` is automatically a `ConditionallyCompletePartialOrder`. Because of the `to_dual` attribute, the additional overhead required to add and maintain the infimum version is minimal.
rao107
pushed a commit
to rao107/mathlib4
that referenced
this pull request
Feb 18, 2026
…y#35046) This file defines *conditionally complete partial orders* with suprema, infima or both. These are partial orders where every nonempty, upwards (downwards) directed set which is bounded above (below) has a least upper bound (greatest lower bound). This class extends `SupSet` (`InfSet`) and the requirement is that `sSup` (`sInf`) must be the least upper bound. The three classes defined herein are: + `ConditionallyCompletePartialOrderSup` for partial orders with suprema, + `ConditionallyCompletePartialOrderInf` for partial orders with infima, and + `ConditionallyCompletePartialOrder` for partial orders with both suprema and infima One common use case for these classes is the order on a von Neumann algebra, or W⋆-algebra. This is the strongest order-theoretic structure satisfied by a von Neumann algebra; in particular it is *not* a conditionally complete *lattice*, and indeed it is a lattice if and only if the algebra is commutative. In addition, `ℂ` can be made to satisfy this class (one must provide a suitable `SupSet` instance), with the order `w ≤ z ↔ w.re ≤ z.re ∧ w.im = z.im`, which is available in the `ComplexOrder` namespace. These use cases are the motivation for defining three classes, as compared with other parts of the order theory library, where only the supremum versions are defined (e.g., `CompletePartialOrder` and `OmegaCompletePartialOrder`). We note that, if these classes are used outside of order theory, then it is more likely that the infimum versions would be useful. Indeed, whenever the underlying type has an antitone involution (e.g., if it is an ordered ring, then negation would be such a map), then any `ConditionallyCompletePartialOrder{Sup,Inf}` is automatically a `ConditionallyCompletePartialOrder`. Because of the `to_dual` attribute, the additional overhead required to add and maintain the infimum version is minimal.
Maldooor
pushed a commit
to Maldooor/mathlib4
that referenced
this pull request
Feb 25, 2026
…y#35046) This file defines *conditionally complete partial orders* with suprema, infima or both. These are partial orders where every nonempty, upwards (downwards) directed set which is bounded above (below) has a least upper bound (greatest lower bound). This class extends `SupSet` (`InfSet`) and the requirement is that `sSup` (`sInf`) must be the least upper bound. The three classes defined herein are: + `ConditionallyCompletePartialOrderSup` for partial orders with suprema, + `ConditionallyCompletePartialOrderInf` for partial orders with infima, and + `ConditionallyCompletePartialOrder` for partial orders with both suprema and infima One common use case for these classes is the order on a von Neumann algebra, or W⋆-algebra. This is the strongest order-theoretic structure satisfied by a von Neumann algebra; in particular it is *not* a conditionally complete *lattice*, and indeed it is a lattice if and only if the algebra is commutative. In addition, `ℂ` can be made to satisfy this class (one must provide a suitable `SupSet` instance), with the order `w ≤ z ↔ w.re ≤ z.re ∧ w.im = z.im`, which is available in the `ComplexOrder` namespace. These use cases are the motivation for defining three classes, as compared with other parts of the order theory library, where only the supremum versions are defined (e.g., `CompletePartialOrder` and `OmegaCompletePartialOrder`). We note that, if these classes are used outside of order theory, then it is more likely that the infimum versions would be useful. Indeed, whenever the underlying type has an antitone involution (e.g., if it is an ordered ring, then negation would be such a map), then any `ConditionallyCompletePartialOrder{Sup,Inf}` is automatically a `ConditionallyCompletePartialOrder`. Because of the `to_dual` attribute, the additional overhead required to add and maintain the infimum version is minimal.
pfaffelh
pushed a commit
to pfaffelh/mathlib4
that referenced
this pull request
Mar 2, 2026
…y#35046) This file defines *conditionally complete partial orders* with suprema, infima or both. These are partial orders where every nonempty, upwards (downwards) directed set which is bounded above (below) has a least upper bound (greatest lower bound). This class extends `SupSet` (`InfSet`) and the requirement is that `sSup` (`sInf`) must be the least upper bound. The three classes defined herein are: + `ConditionallyCompletePartialOrderSup` for partial orders with suprema, + `ConditionallyCompletePartialOrderInf` for partial orders with infima, and + `ConditionallyCompletePartialOrder` for partial orders with both suprema and infima One common use case for these classes is the order on a von Neumann algebra, or W⋆-algebra. This is the strongest order-theoretic structure satisfied by a von Neumann algebra; in particular it is *not* a conditionally complete *lattice*, and indeed it is a lattice if and only if the algebra is commutative. In addition, `ℂ` can be made to satisfy this class (one must provide a suitable `SupSet` instance), with the order `w ≤ z ↔ w.re ≤ z.re ∧ w.im = z.im`, which is available in the `ComplexOrder` namespace. These use cases are the motivation for defining three classes, as compared with other parts of the order theory library, where only the supremum versions are defined (e.g., `CompletePartialOrder` and `OmegaCompletePartialOrder`). We note that, if these classes are used outside of order theory, then it is more likely that the infimum versions would be useful. Indeed, whenever the underlying type has an antitone involution (e.g., if it is an ordered ring, then negation would be such a map), then any `ConditionallyCompletePartialOrder{Sup,Inf}` is automatically a `ConditionallyCompletePartialOrder`. Because of the `to_dual` attribute, the additional overhead required to add and maintain the infimum version is minimal.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This file defines conditionally complete partial orders with suprema, infima or both. These are partial orders where every nonempty, upwards (downwards) directed set which is bounded above (below) has a least upper bound (greatest lower bound). This class extends
SupSet(InfSet) and the requirement is thatsSup(sInf) must be the least upper bound.The three classes defined herein are:
ConditionallyCompletePartialOrderSupfor partial orders with suprema,ConditionallyCompletePartialOrderInffor partial orders with infima, andConditionallyCompletePartialOrderfor partial orders with both suprema and infimaOne common use case for these classes is the order on a von Neumann algebra, or W⋆-algebra. This is the strongest order-theoretic structure satisfied by a von Neumann algebra; in particular it is not a conditionally complete lattice, and indeed it is a lattice if and only if the algebra is commutative. In addition,
ℂcan be made to satisfy this class (one must provide a suitableSupSetinstance), with the orderw ≤ z ↔ w.re ≤ z.re ∧ w.im = z.im, which is available in theComplexOrdernamespace.These use cases are the motivation for defining three classes, as compared with other parts of the order theory library, where only the supremum versions are defined (e.g.,
CompletePartialOrderandOmegaCompletePartialOrder). We note that, if these classes are used outside of order theory, then it is more likely that the infimum versions would be useful. Indeed, whenever the underlying type has an antitone involution (e.g., if it is an ordered ring, then negation would be such a map), then anyConditionallyCompletePartialOrder{Sup,Inf}is automatically aConditionallyCompletePartialOrder. Because of theto_dualattribute, the additional overhead required to add and maintain the infimum version is minimal.In a follow-up PR, we provide a more robust API and generalize some lemmas from
ConditionallyCompleteLatticetoConditionallyCompletePartialOrder{Sup,Inf}.