Zulip Chat Archive

Stream: general

Topic: neg


view this post on Zulip Johan Commelin (May 27 2020 at 11:25):

I love the name of this lemma:

@[simp] lemma neg_neg_iff_pos : -a < 0  0 < a :=

view this post on Zulip Kevin Buzzard (May 27 2020 at 11:36):

ooh we have a naming convention clash?

view this post on Zulip Mario Carneiro (May 27 2020 at 11:37):

yep

view this post on Zulip Mario Carneiro (May 27 2020 at 11:37):

I use lt_zero when this comes up

view this post on Zulip Anne Baanen (May 27 2020 at 11:40):

Since pos and nonpos don't cause conflicts, how about nonneg and nonnonneg?


Last updated: May 09 2021 at 19:11 UTC