Zulip Chat Archive

Stream: maths

Topic: order_dual disappointment


view this post on Zulip Chris Hughes (Jun 28 2019 at 14:24):

How sad...

example (a b : β) : max a b = @min (order_dual β) _ a b := rfl --doesn't work

view this post on Zulip Kenny Lau (Jun 28 2019 at 18:55):

import order.basic
variables (β : Type*) [decidable_linear_order β]
example (a b : β) : max a b = @min (order_dual β) _ b a := rfl --works

view this post on Zulip Chris Hughes (Jun 28 2019 at 18:57):

I might go and change the definition of list.maximum, with this in mind, and swap the order


Last updated: May 06 2021 at 19:30 UTC