Zulip Chat Archive

Stream: new members

Topic: decreasing function


Horatiu Cheval (Feb 19 2021 at 06:52):

What's the proper way of saying that a function ℝ → ℝ is decreasing using monotone?
Do I do something like this

import data.real.basic

def ge_preorder : preorder  :=
{
  le := (λ x y : , x  y),
  -- and so on, filling in the rest of the axioms
}

def decreasing (f :   ) : Prop := @monotone   real.preorder ge_preorder f

or is there something built-in in mathlib?

Mario Carneiro (Feb 19 2021 at 07:30):

You can use order_dual real for the reverse preorder

Mario Carneiro (Feb 19 2021 at 07:30):

so something like monotone (f \circ order_dual.mk)

Horatiu Cheval (Feb 19 2021 at 07:43):

Ok, thanks, that's much nicer


Last updated: Dec 20 2023 at 11:08 UTC