## 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

#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: May 13 2021 at 19:20 UTC