Zulip Chat Archive

Stream: general

Topic: strictly monotone


view this post on Zulip 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 < ... <?

view this post on Zulip Reid Barton (May 13 2019 at 12:58):

oh, it's strict_mono in a different place

view this post on Zulip Mario Carneiro (May 13 2019 at 13:00):

I think there's a PR about this

view this post on Zulip Reid Barton (May 13 2019 at 13:02):

#998

view this post on Zulip Reid Barton (May 13 2019 at 13:05):

Perhaps it should move to order/

view this post on Zulip 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: May 13 2021 at 19:20 UTC