Zulip Chat Archive

Stream: general

Topic: missing lemmas for inf?


view this post on Zulip Johan Commelin (Jul 29 2019 at 20:16):

Both of these fail:

example (m n : ) (h : m < n) : m = m  n := by library_search
example (m n : ) (h : m < n) : m  m  n := by library_search

view this post on Zulip Chris Hughes (Jul 29 2019 at 20:20):

I bet they work with le

view this post on Zulip Chris Hughes (Jul 29 2019 at 20:21):

Instead of lt

view this post on Zulip Johan Commelin (Jul 29 2019 at 20:34):

How much do you want to bet :stuck_out_tongue_wink:

view this post on Zulip Mario Carneiro (Jul 29 2019 at 23:01):

the equality is the other way around, I think this is inf_of_le_left. The second one is just a composition of this with le_of_eq


Last updated: May 08 2021 at 19:11 UTC