Zulip Chat Archive

Stream: maths

Topic: ordered_comm_monoid


view this post on Zulip Yury G. Kudryashov (Jul 30 2020 at 05:39):

I want to add two typeclasses:

@[to_additive]
class weakly_ordered_comm_monoid (α : Type*) extends comm_monoid α, partial_order α :=
(mul_le_mul_left       :  a b : α, a  b   c : α, c * a  c * b)

class canonically_weakly_ordered_add_monoid (α : Type*) extends weakly_ordered_add_comm_monoid α, order_bot α :=
(le_iff_exists_add : a b:α, a  b  c, b = a + c)

The main use cases for the second class are measure α and α → enreal. The axiom

(lt_of_add_lt_add_left :  a b c : α, a + b < a + c  b < c)

doesn't work in these cases. E.g., for bool → ennreal the counterexample is given by a = λ x, cond x 0 ∞, b = λ x, cond x 0 1, c = λ x, cond x 1 0, a + b = λ x, cond x 0 ∞, a + c = λ x, cond x 1 ∞.

What do you think about this? Do you have better names for these classes?

view this post on Zulip Johan Commelin (Jul 30 2020 at 05:46):

I think those are useful. I'm just starting to wonder if we should transition to mixins in the order-meets-algebra part of the library...


Last updated: May 09 2021 at 10:11 UTC