Zulip Chat Archive
Stream: general
Topic: neg
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 :=
Kevin Buzzard (May 27 2020 at 11:36):
ooh we have a naming convention clash?
Mario Carneiro (May 27 2020 at 11:37):
yep
Mario Carneiro (May 27 2020 at 11:37):
I use lt_zero when this comes up
Anne Baanen (May 27 2020 at 11:40):
Since pos and nonpos don't cause conflicts, how about nonneg and nonnonneg?
Last updated: Dec 20 2023 at 11:08 UTC