monotone

Stream: general

[Kenny Lau]

sehr geehrter @Johannes Hölzl , monotone doesn't mean what you think it means

[Johannes Hölzl]

What is the difference between https://github.com/leanprover/mathlib/blob/master/order/basic.lean#L19
def monotone (f : α → β) := ∀⦃a b⦄, a ≤ b → f a ≤ f b
and
class is_ord_hom (f : α → α) : Prop := (ord : ∀ x y, x ≤ y → f x ≤ f y) ?
Monotone is a little bit more general, but not a type class...

[Kenny Lau]

@Johannes Hölzl monotone means increasing or decreasing

[Kenny Lau]

at least in where I'm from

[Johannes Hölzl]

Not in order theory, the "Monotonicity in order theory" section in https://en.wikipedia.org/wiki/Monotonic_function tells us that it means what you maybe call an increasing function.

[Kenny Lau]

fair enough