Zulip Chat Archive
Stream: general
Topic: missing lemmas for inf?
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
Chris Hughes (Jul 29 2019 at 20:20):
I bet they work with le
Chris Hughes (Jul 29 2019 at 20:21):
Instead of lt
Johan Commelin (Jul 29 2019 at 20:34):
How much do you want to bet :stuck_out_tongue_wink:
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: Dec 20 2023 at 11:08 UTC