Zulip Chat Archive

Stream: new members

Topic: ordering


view this post on Zulip Iocta (Jul 09 2020 at 04:51):

I have a bunch of < and <= relations, and I want to combine them into a chain automatically, is there a tactic for this?

view this post on Zulip Iocta (Jul 09 2020 at 04:54):

ie all the lt_trans-like commands combined

view this post on Zulip Bryan Gin-ge Chen (Jul 09 2020 at 04:54):

You could write them in a calc block.

view this post on Zulip Bryan Gin-ge Chen (Jul 09 2020 at 04:55):

https://leanprover-community.github.io/extras/calc.html

view this post on Zulip Reid Barton (Jul 09 2020 at 12:07):

If you don't want to write the steps explicitly, linarith might work (not sure if it requires some extra structure on the ordering that you might not have but most likely do). I think mono might work as well.


Last updated: May 17 2021 at 23:14 UTC