Zulip Chat Archive

Stream: general

Topic: strictly monotone

Reid Barton (May 13 2019 at 12:57):

We have def monotone (f : α → β) := ∀⦃a b⦄, a ≤ b → f a ≤ f b, but is there a version with < ... <?

Reid Barton (May 13 2019 at 12:58):

oh, it's strict_mono in a different place

Mario Carneiro (May 13 2019 at 13:00):

I think there's a PR about this

Reid Barton (May 13 2019 at 13:02):

#998

Reid Barton (May 13 2019 at 13:05):

Perhaps it should move to order/

Kevin Buzzard (May 13 2019 at 15:05):

This is one of the infinitely many PR's coming from the perfectoid project :D

Last updated: Dec 20 2023 at 11:08 UTC