decreasing function

Stream: new members

[Horatiu Cheval]

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]

You can use order_dual real for the reverse preorder

[Mario Carneiro]

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

[Horatiu Cheval]

Ok, thanks, that's much nicer