Semigroups of real numbers under the min/max operators #1631
Conversation
| associative-max-ℝ : max-ℝ (max-ℝ x y) z ＝ max-ℝ x (max-ℝ y z) | ||
| associative-max-ℝ = |
There was a problem hiding this comment.
This is true in any large poset with meets, by the same argument as you demonstrate. Would you be willing to prove it in that generality, if it is not already?
There was a problem hiding this comment.
As a corollary, any large poset has an associated large semigroup under max.
| associative-min-ℝ : min-ℝ (min-ℝ x y) z ＝ min-ℝ x (min-ℝ y z) | ||
| associative-min-ℝ = | ||
| antisymmetric-leq-ℝ | ||
| ( min-ℝ (min-ℝ x y) z) | ||
| ( min-ℝ x (min-ℝ y z)) |
There was a problem hiding this comment.
Same comment here. this is true by the same proof that you write in all large posets with joins.
There was a problem hiding this comment.
As a corollary, any large poset has an associated large semigroup under min.
Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>
Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>
|
There are weird things going on in the large meet/join semilattices modules: headers are awkwardly asymmetric and don't describe what is actually defined in the module. |
2 participants
This PR introduces the large semigroups of real numbers under the min / max binary operators.