# mathlibdocumentation

order.monotone.basic

# Monotonicity #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines (strictly) monotone/antitone functions. Contrary to standard mathematical usage, "monotone"/"mono" here means "increasing", not "increasing or decreasing". We use "antitone"/"anti" to mean "decreasing".

## Definitions #

• `monotone f`: A function `f` between two preorders is monotone if `a ≤ b` implies `f a ≤ f b`.
• `antitone f`: A function `f` between two preorders is antitone if `a ≤ b` implies `f b ≤ f a`.
• `monotone_on f s`: Same as `monotone f`, but for all `a, b ∈ s`.
• `antitone_on f s`: Same as `antitone f`, but for all `a, b ∈ s`.
• `strict_mono f` : A function `f` between two preorders is strictly monotone if `a < b` implies `f a < f b`.
• `strict_anti f` : A function `f` between two preorders is strictly antitone if `a < b` implies `f b < f a`.
• `strict_mono_on f s`: Same as `strict_mono f`, but for all `a, b ∈ s`.
• `strict_anti_on f s`: Same as `strict_anti f`, but for all `a, b ∈ s`.

## Main theorems #

• `monotone_nat_of_le_succ`, `monotone_int_of_le_succ`: If `f : ℕ → α` or `f : ℤ → α` and `f n ≤ f (n + 1)` for all `n`, then `f` is monotone.
• `antitone_nat_of_succ_le`, `antitone_int_of_succ_le`: If `f : ℕ → α` or `f : ℤ → α` and `f (n + 1) ≤ f n` for all `n`, then `f` is antitone.
• `strict_mono_nat_of_lt_succ`, `strict_mono_int_of_lt_succ`: If `f : ℕ → α` or `f : ℤ → α` and `f n < f (n + 1)` for all `n`, then `f` is strictly monotone.
• `strict_anti_nat_of_succ_lt`, `strict_anti_int_of_succ_lt`: If `f : ℕ → α` or `f : ℤ → α` and `f (n + 1) < f n` for all `n`, then `f` is strictly antitone.

## Implementation notes #

Some of these definitions used to only require `has_le α` or `has_lt α`. The advantage of this is unclear and it led to slight elaboration issues. Now, everything requires `preorder α` and seems to work fine. Related Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Order.20diamond/near/254353352.

## TODO #

The above theorems are also true in `ℕ+`, `fin n`... To make that work, we need `succ_order α` and `succ_archimedean α`.

## Tags #

monotone, strictly monotone, antitone, strictly antitone, increasing, strictly increasing, decreasing, strictly decreasing

def monotone {α : Type u} {β : Type v} [preorder α] [preorder β] (f : α β) :
Prop

A function `f` is monotone if `a ≤ b` implies `f a ≤ f b`.

Equations
Instances for `monotone`
def antitone {α : Type u} {β : Type v} [preorder α] [preorder β] (f : α β) :
Prop

A function `f` is antitone if `a ≤ b` implies `f b ≤ f a`.

Equations
Instances for `antitone`
def monotone_on {α : Type u} {β : Type v} [preorder α] [preorder β] (f : α β) (s : set α) :
Prop

A function `f` is monotone on `s` if, for all `a, b ∈ s`, `a ≤ b` implies `f a ≤ f b`.

Equations
def antitone_on {α : Type u} {β : Type v} [preorder α] [preorder β] (f : α β) (s : set α) :
Prop

A function `f` is antitone on `s` if, for all `a, b ∈ s`, `a ≤ b` implies `f b ≤ f a`.

Equations
def strict_mono {α : Type u} {β : Type v} [preorder α] [preorder β] (f : α β) :
Prop

A function `f` is strictly monotone if `a < b` implies `f a < f b`.

Equations
def strict_anti {α : Type u} {β : Type v} [preorder α] [preorder β] (f : α β) :
Prop

A function `f` is strictly antitone if `a < b` implies `f b < f a`.

Equations
def strict_mono_on {α : Type u} {β : Type v} [preorder α] [preorder β] (f : α β) (s : set α) :
Prop

A function `f` is strictly monotone on `s` if, for all `a, b ∈ s`, `a < b` implies `f a < f b`.

Equations
def strict_anti_on {α : Type u} {β : Type v} [preorder α] [preorder β] (f : α β) (s : set α) :
Prop

A function `f` is strictly antitone on `s` if, for all `a, b ∈ s`, `a < b` implies `f b < f a`.

Equations

### Monotonicity on the dual order #

Strictly, many of the `*_on.dual` lemmas in this section should use `of_dual ⁻¹' s` instead of `s`, but right now this is not possible as `set.preimage` is not defined yet, and importing it creates an import cycle.

Often, you should not need the rewriting lemmas. Instead, you probably want to add `.dual`, `.dual_left` or `.dual_right` to your `monotone`/`antitone` hypothesis.

@[simp]
theorem monotone_comp_of_dual_iff {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α β} :
@[simp]
theorem antitone_comp_of_dual_iff {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α β} :
@[simp]
theorem monotone_to_dual_comp_iff {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α β} :
@[simp]
theorem antitone_to_dual_comp_iff {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α β} :
@[simp]
theorem monotone_on_comp_of_dual_iff {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α β} {s : set α} :
s
@[simp]
theorem antitone_on_comp_of_dual_iff {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α β} {s : set α} :
s
@[simp]
theorem monotone_on_to_dual_comp_iff {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α β} {s : set α} :
s
@[simp]
theorem antitone_on_to_dual_comp_iff {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α β} {s : set α} :
s
@[simp]
theorem strict_mono_comp_of_dual_iff {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α β} :
@[simp]
theorem strict_anti_comp_of_dual_iff {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α β} :
@[simp]
theorem strict_mono_to_dual_comp_iff {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α β} :
@[simp]
theorem strict_anti_to_dual_comp_iff {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α β} :
@[simp]
theorem strict_mono_on_comp_of_dual_iff {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α β} {s : set α} :
@[simp]
theorem strict_anti_on_comp_of_dual_iff {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α β} {s : set α} :
@[simp]
theorem strict_mono_on_to_dual_comp_iff {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α β} {s : set α} :
@[simp]
theorem strict_anti_on_to_dual_comp_iff {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α β} {s : set α} :
@[protected]
theorem monotone.dual {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α β} (hf : monotone f) :
@[protected]
theorem antitone.dual {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α β} (hf : antitone f) :
@[protected]
theorem monotone_on.dual {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α β} {s : set α} (hf : s) :
@[protected]
theorem antitone_on.dual {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α β} {s : set α} (hf : s) :
@[protected]
theorem strict_mono.dual {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α β} (hf : strict_mono f) :
@[protected]
theorem strict_anti.dual {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α β} (hf : strict_anti f) :
@[protected]
theorem strict_mono_on.dual {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α β} {s : set α} (hf : s) :
@[protected]
theorem strict_anti_on.dual {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α β} {s : set α} (hf : s) :
theorem monotone.dual_left {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α β} :

Alias of the reverse direction of `antitone_comp_of_dual_iff`.

theorem antitone.dual_left {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α β} :

Alias of the reverse direction of `monotone_comp_of_dual_iff`.

theorem monotone.dual_right {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α β} :

Alias of the reverse direction of `antitone_to_dual_comp_iff`.

theorem antitone.dual_right {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α β} :

Alias of the reverse direction of `monotone_to_dual_comp_iff`.

theorem monotone_on.dual_left {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α β} {s : set α} :
s

Alias of the reverse direction of `antitone_on_comp_of_dual_iff`.

theorem antitone_on.dual_left {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α β} {s : set α} :
s

Alias of the reverse direction of `monotone_on_comp_of_dual_iff`.

theorem monotone_on.dual_right {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α β} {s : set α} :
s

Alias of the reverse direction of `antitone_on_to_dual_comp_iff`.

theorem antitone_on.dual_right {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α β} {s : set α} :
s

Alias of the reverse direction of `monotone_on_to_dual_comp_iff`.

theorem strict_mono.dual_left {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α β} :

Alias of the reverse direction of `strict_anti_comp_of_dual_iff`.

theorem strict_anti.dual_left {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α β} :

Alias of the reverse direction of `strict_mono_comp_of_dual_iff`.

theorem strict_mono.dual_right {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α β} :

Alias of the reverse direction of `strict_anti_to_dual_comp_iff`.

theorem strict_anti.dual_right {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α β} :

Alias of the reverse direction of `strict_mono_to_dual_comp_iff`.

theorem strict_mono_on.dual_left {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α β} {s : set α} :

Alias of the reverse direction of `strict_anti_on_comp_of_dual_iff`.

theorem strict_anti_on.dual_left {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α β} {s : set α} :

Alias of the reverse direction of `strict_mono_on_comp_of_dual_iff`.

theorem strict_mono_on.dual_right {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α β} {s : set α} :

Alias of the reverse direction of `strict_anti_on_to_dual_comp_iff`.

theorem strict_anti_on.dual_right {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α β} {s : set α} :

Alias of the reverse direction of `strict_mono_on_to_dual_comp_iff`.

### Monotonicity in function spaces #

theorem monotone.comp_le_comp_left {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder β] {f : β α} {g h : γ β} (hf : monotone f) (le_gh : g h) :
f g f h
theorem monotone_lam {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder γ] {f : α β γ} (hf : (b : β), monotone (λ (a : α), f a b)) :
theorem monotone_app {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder γ] (f : β α γ) (b : β) (hf : monotone (λ (a : α) (b : β), f b a)) :
monotone (f b)
theorem antitone_lam {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder γ] {f : α β γ} (hf : (b : β), antitone (λ (a : α), f a b)) :
theorem antitone_app {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder γ] (f : β α γ) (b : β) (hf : antitone (λ (a : α) (b : β), f b a)) :
antitone (f b)
theorem function.monotone_eval {ι : Type u} {α : ι Type v} [Π (i : ι), preorder (α i)] (i : ι) :

### Monotonicity hierarchy #

These four lemmas are there to strip off the semi-implicit arguments `⦃a b : α⦄`. This is useful when you do not want to apply a `monotone` assumption (i.e. your goal is `a ≤ b → f a ≤ f b`). However if you find yourself writing `hf.imp h`, then you should have written `hf h` instead.

theorem monotone.imp {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α β} {a b : α} (hf : monotone f) (h : a b) :
f a f b
theorem antitone.imp {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α β} {a b : α} (hf : antitone f) (h : a b) :
f b f a
theorem strict_mono.imp {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α β} {a b : α} (hf : strict_mono f) (h : a < b) :
f a < f b
theorem strict_anti.imp {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α β} {a b : α} (hf : strict_anti f) (h : a < b) :
f b < f a
@[protected]
theorem monotone.monotone_on {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α β} (hf : monotone f) (s : set α) :
s
@[protected]
theorem antitone.antitone_on {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α β} (hf : antitone f) (s : set α) :
s
@[simp]
theorem monotone_on_univ {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α β} :
@[simp]
theorem antitone_on_univ {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α β} :
@[protected]
theorem strict_mono.strict_mono_on {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α β} (hf : strict_mono f) (s : set α) :
@[protected]
theorem strict_anti.strict_anti_on {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α β} (hf : strict_anti f) (s : set α) :
@[simp]
theorem strict_mono_on_univ {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α β} :
@[simp]
theorem strict_anti_on_univ {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α β} :
theorem monotone.strict_mono_of_injective {α : Type u} {β : Type v} [preorder α] {f : α β} (h₁ : monotone f) (h₂ : function.injective f) :
theorem antitone.strict_anti_of_injective {α : Type u} {β : Type v} [preorder α] {f : α β} (h₁ : antitone f) (h₂ : function.injective f) :
theorem monotone_iff_forall_lt {α : Type u} {β : Type v} [preorder β] {f : α β} :
⦃a b : α⦄, a < b f a f b
theorem antitone_iff_forall_lt {α : Type u} {β : Type v} [preorder β] {f : α β} :
⦃a b : α⦄, a < b f b f a
theorem monotone_on_iff_forall_lt {α : Type u} {β : Type v} [preorder β] {f : α β} {s : set α} :
s ⦃a : α⦄, a s ⦃b : α⦄, b s a < b f a f b
theorem antitone_on_iff_forall_lt {α : Type u} {β : Type v} [preorder β] {f : α β} {s : set α} :
s ⦃a : α⦄, a s ⦃b : α⦄, b s a < b f b f a
@[protected]
theorem strict_mono_on.monotone_on {α : Type u} {β : Type v} [preorder β] {f : α β} {s : set α} (hf : s) :
s
@[protected]
theorem strict_anti_on.antitone_on {α : Type u} {β : Type v} [preorder β] {f : α β} {s : set α} (hf : s) :
s
@[protected]
theorem strict_mono.monotone {α : Type u} {β : Type v} [preorder β] {f : α β} (hf : strict_mono f) :
@[protected]
theorem strict_anti.antitone {α : Type u} {β : Type v} [preorder β] {f : α β} (hf : strict_anti f) :

### Monotonicity from and to subsingletons #

@[protected]
theorem subsingleton.monotone {α : Type u} {β : Type v} [preorder α] [preorder β] [subsingleton α] (f : α β) :
@[protected]
theorem subsingleton.antitone {α : Type u} {β : Type v} [preorder α] [preorder β] [subsingleton α] (f : α β) :
theorem subsingleton.monotone' {α : Type u} {β : Type v} [preorder α] [preorder β] [subsingleton β] (f : α β) :
theorem subsingleton.antitone' {α : Type u} {β : Type v} [preorder α] [preorder β] [subsingleton β] (f : α β) :
@[protected]
theorem subsingleton.strict_mono {α : Type u} {β : Type v} [preorder α] [preorder β] [subsingleton α] (f : α β) :
@[protected]
theorem subsingleton.strict_anti {α : Type u} {β : Type v} [preorder α] [preorder β] [subsingleton α] (f : α β) :

### Miscellaneous monotonicity results #

theorem monotone_id {α : Type u} [preorder α] :
theorem monotone_on_id {α : Type u} [preorder α] {s : set α} :
theorem strict_mono_id {α : Type u} [preorder α] :
theorem strict_mono_on_id {α : Type u} [preorder α] {s : set α} :
theorem monotone_const {α : Type u} {β : Type v} [preorder α] [preorder β] {c : β} :
monotone (λ (a : α), c)
theorem monotone_on_const {α : Type u} {β : Type v} [preorder α] [preorder β] {c : β} {s : set α} :
monotone_on (λ (a : α), c) s
theorem antitone_const {α : Type u} {β : Type v} [preorder α] [preorder β] {c : β} :
antitone (λ (a : α), c)
theorem antitone_on_const {α : Type u} {β : Type v} [preorder α] [preorder β] {c : β} {s : set α} :
antitone_on (λ (a : α), c) s
theorem strict_mono_of_le_iff_le {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α β} (h : (x y : α), x y f x f y) :
theorem strict_anti_of_le_iff_le {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α β} (h : (x y : α), x y f y f x) :
theorem injective_of_lt_imp_ne {α : Type u} {β : Type v} [linear_order α] {f : α β} (h : (x y : α), x < y f x f y) :
theorem injective_of_le_imp_le {α : Type u} {β : Type v} [preorder β] (f : α β) (h : {x y : α}, f x f y x y) :
theorem strict_mono.is_max_of_apply {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α β} {a : α} (hf : strict_mono f) (ha : is_max (f a)) :
theorem strict_mono.is_min_of_apply {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α β} {a : α} (hf : strict_mono f) (ha : is_min (f a)) :
theorem strict_anti.is_max_of_apply {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α β} {a : α} (hf : strict_anti f) (ha : is_min (f a)) :
theorem strict_anti.is_min_of_apply {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α β} {a : α} (hf : strict_anti f) (ha : is_max (f a)) :
@[protected]
theorem strict_mono.ite' {α : Type u} {β : Type v} [preorder α] [preorder β] {f g : α β} (hf : strict_mono f) (hg : strict_mono g) {p : α Prop} (hp : ⦃x y : α⦄, x < y p y p x) (hfg : ⦃x y : α⦄, p x ¬p y x < y f x < g y) :
strict_mono (λ (x : α), ite (p x) (f x) (g x))
@[protected]
theorem strict_mono.ite {α : Type u} {β : Type v} [preorder α] [preorder β] {f g : α β} (hf : strict_mono f) (hg : strict_mono g) {p : α Prop} (hp : ⦃x y : α⦄, x < y p y p x) (hfg : (x : α), f x g x) :
strict_mono (λ (x : α), ite (p x) (f x) (g x))
@[protected]
theorem strict_anti.ite' {α : Type u} {β : Type v} [preorder α] [preorder β] {f g : α β} (hf : strict_anti f) (hg : strict_anti g) {p : α Prop} (hp : ⦃x y : α⦄, x < y p y p x) (hfg : ⦃x y : α⦄, p x ¬p y x < y g y < f x) :
strict_anti (λ (x : α), ite (p x) (f x) (g x))
@[protected]
theorem strict_anti.ite {α : Type u} {β : Type v} [preorder α] [preorder β] {f g : α β} (hf : strict_anti f) (hg : strict_anti g) {p : α Prop} (hp : ⦃x y : α⦄, x < y p y p x) (hfg : (x : α), g x f x) :
strict_anti (λ (x : α), ite (p x) (f x) (g x))

### Monotonicity under composition #

@[protected]
theorem monotone.comp {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder β] [preorder γ] {g : β γ} {f : α β} (hg : monotone g) (hf : monotone f) :
theorem monotone.comp_antitone {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder β] [preorder γ] {g : β γ} {f : α β} (hg : monotone g) (hf : antitone f) :
@[protected]
theorem antitone.comp {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder β] [preorder γ] {g : β γ} {f : α β} (hg : antitone g) (hf : antitone f) :
theorem antitone.comp_monotone {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder β] [preorder γ] {g : β γ} {f : α β} (hg : antitone g) (hf : monotone f) :
@[protected]
theorem monotone.iterate {α : Type u} [preorder α] {f : α α} (hf : monotone f) (n : ) :
@[protected]
theorem monotone.comp_monotone_on {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder β] [preorder γ] {g : β γ} {f : α β} {s : set α} (hg : monotone g) (hf : s) :
theorem monotone.comp_antitone_on {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder β] [preorder γ] {g : β γ} {f : α β} {s : set α} (hg : monotone g) (hf : s) :
@[protected]
theorem antitone.comp_antitone_on {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder β] [preorder γ] {g : β γ} {f : α β} {s : set α} (hg : antitone g) (hf : s) :
theorem antitone.comp_monotone_on {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder β] [preorder γ] {g : β γ} {f : α β} {s : set α} (hg : antitone g) (hf : s) :
@[protected]
theorem strict_mono.comp {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder β] [preorder γ] {g : β γ} {f : α β} (hg : strict_mono g) (hf : strict_mono f) :
theorem strict_mono.comp_strict_anti {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder β] [preorder γ] {g : β γ} {f : α β} (hg : strict_mono g) (hf : strict_anti f) :
@[protected]
theorem strict_anti.comp {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder β] [preorder γ] {g : β γ} {f : α β} (hg : strict_anti g) (hf : strict_anti f) :
theorem strict_anti.comp_strict_mono {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder β] [preorder γ] {g : β γ} {f : α β} (hg : strict_anti g) (hf : strict_mono f) :
@[protected]
theorem strict_mono.iterate {α : Type u} [preorder α] {f : α α} (hf : strict_mono f) (n : ) :
@[protected]
theorem strict_mono.comp_strict_mono_on {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder β] [preorder γ] {g : β γ} {f : α β} {s : set α} (hg : strict_mono g) (hf : s) :
theorem strict_mono.comp_strict_anti_on {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder β] [preorder γ] {g : β γ} {f : α β} {s : set α} (hg : strict_mono g) (hf : s) :
@[protected]
theorem strict_anti.comp_strict_anti_on {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder β] [preorder γ] {g : β γ} {f : α β} {s : set α} (hg : strict_anti g) (hf : s) :
theorem strict_anti.comp_strict_mono_on {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder β] [preorder γ] {g : β γ} {f : α β} {s : set α} (hg : strict_anti g) (hf : s) :
theorem list.foldl_monotone {α : Type u} {β : Type v} [preorder α] {f : α β α} (H : (b : β), monotone (λ (a : α), f a b)) (l : list β) :
monotone (λ (a : α), a l)
theorem list.foldr_monotone {α : Type u} {β : Type v} [preorder β] {f : α β β} (H : (a : α), monotone (f a)) (l : list α) :
monotone (λ (b : β), b l)
theorem list.foldl_strict_mono {α : Type u} {β : Type v} [preorder α] {f : α β α} (H : (b : β), strict_mono (λ (a : α), f a b)) (l : list β) :
strict_mono (λ (a : α), a l)
theorem list.foldr_strict_mono {α : Type u} {β : Type v} [preorder β] {f : α β β} (H : (a : α), strict_mono (f a)) (l : list α) :
strict_mono (λ (b : β), b l)

### Monotonicity in linear orders #

theorem monotone.reflect_lt {α : Type u} {β : Type v} [linear_order α] [preorder β] {f : α β} (hf : monotone f) {a b : α} (h : f a < f b) :
a < b
theorem antitone.reflect_lt {α : Type u} {β : Type v} [linear_order α] [preorder β] {f : α β} (hf : antitone f) {a b : α} (h : f a < f b) :
b < a
theorem monotone_on.reflect_lt {α : Type u} {β : Type v} [linear_order α] [preorder β] {f : α β} {s : set α} (hf : s) {a b : α} (ha : a s) (hb : b s) (h : f a < f b) :
a < b
theorem antitone_on.reflect_lt {α : Type u} {β : Type v} [linear_order α] [preorder β] {f : α β} {s : set α} (hf : s) {a b : α} (ha : a s) (hb : b s) (h : f a < f b) :
b < a
theorem strict_mono_on.le_iff_le {α : Type u} {β : Type v} [linear_order α] [preorder β] {f : α β} {s : set α} (hf : s) {a b : α} (ha : a s) (hb : b s) :
f a f b a b
theorem strict_anti_on.le_iff_le {α : Type u} {β : Type v} [linear_order α] [preorder β] {f : α β} {s : set α} (hf : s) {a b : α} (ha : a s) (hb : b s) :
f a f b b a
theorem strict_mono_on.eq_iff_eq {α : Type u} {β : Type v} [linear_order α] [preorder β] {f : α β} {s : set α} (hf : s) {a b : α} (ha : a s) (hb : b s) :
f a = f b a = b
theorem strict_anti_on.eq_iff_eq {α : Type u} {β : Type v} [linear_order α] [preorder β] {f : α β} {s : set α} (hf : s) {a b : α} (ha : a s) (hb : b s) :
f a = f b b = a
theorem strict_mono_on.lt_iff_lt {α : Type u} {β : Type v} [linear_order α] [preorder β] {f : α β} {s : set α} (hf : s) {a b : α} (ha : a s) (hb : b s) :
f a < f b a < b
theorem strict_anti_on.lt_iff_lt {α : Type u} {β : Type v} [linear_order α] [preorder β] {f : α β} {s : set α} (hf : s) {a b : α} (ha : a s) (hb : b s) :
f a < f b b < a
theorem strict_mono.le_iff_le {α : Type u} {β : Type v} [linear_order α] [preorder β] {f : α β} (hf : strict_mono f) {a b : α} :
f a f b a b
theorem strict_anti.le_iff_le {α : Type u} {β : Type v} [linear_order α] [preorder β] {f : α β} (hf : strict_anti f) {a b : α} :
f a f b b a
theorem strict_mono.lt_iff_lt {α : Type u} {β : Type v} [linear_order α] [preorder β] {f : α β} (hf : strict_mono f) {a b : α} :
f a < f b a < b
theorem strict_anti.lt_iff_lt {α : Type u} {β : Type v} [linear_order α] [preorder β] {f : α β} (hf : strict_anti f) {a b : α} :
f a < f b b < a
@[protected]
theorem strict_mono_on.compares {α : Type u} {β : Type v} [linear_order α] [preorder β] {f : α β} {s : set α} (hf : s) {a b : α} (ha : a s) (hb : b s) {o : ordering} :
o.compares (f a) (f b) o.compares a b
@[protected]
theorem strict_anti_on.compares {α : Type u} {β : Type v} [linear_order α] [preorder β] {f : α β} {s : set α} (hf : s) {a b : α} (ha : a s) (hb : b s) {o : ordering} :
o.compares (f a) (f b) o.compares b a
@[protected]
theorem strict_mono.compares {α : Type u} {β : Type v} [linear_order α] [preorder β] {f : α β} (hf : strict_mono f) {a b : α} {o : ordering} :
o.compares (f a) (f b) o.compares a b
@[protected]
theorem strict_anti.compares {α : Type u} {β : Type v} [linear_order α] [preorder β] {f : α β} (hf : strict_anti f) {a b : α} {o : ordering} :
o.compares (f a) (f b) o.compares b a
theorem strict_mono.injective {α : Type u} {β : Type v} [linear_order α] [preorder β] {f : α β} (hf : strict_mono f) :
theorem strict_anti.injective {α : Type u} {β : Type v} [linear_order α] [preorder β] {f : α β} (hf : strict_anti f) :
theorem strict_mono.maximal_of_maximal_image {α : Type u} {β : Type v} [linear_order α] [preorder β] {f : α β} (hf : strict_mono f) {a : α} (hmax : (p : β), p f a) (x : α) :
x a
theorem strict_mono.minimal_of_minimal_image {α : Type u} {β : Type v} [linear_order α] [preorder β] {f : α β} (hf : strict_mono f) {a : α} (hmin : (p : β), f a p) (x : α) :
a x
theorem strict_anti.minimal_of_maximal_image {α : Type u} {β : Type v} [linear_order α] [preorder β] {f : α β} (hf : strict_anti f) {a : α} (hmax : (p : β), p f a) (x : α) :
a x
theorem strict_anti.maximal_of_minimal_image {α : Type u} {β : Type v} [linear_order α] [preorder β] {f : α β} (hf : strict_anti f) {a : α} (hmin : (p : β), f a p) (x : α) :
x a
theorem monotone.strict_mono_iff_injective {α : Type u} {β : Type v} [linear_order α] {f : α β} (hf : monotone f) :
theorem antitone.strict_anti_iff_injective {α : Type u} {β : Type v} [linear_order α] {f : α β} (hf : antitone f) :
theorem not_monotone_not_antitone_iff_exists_le_le {α : Type u} {β : Type v} [linear_order α] [linear_order β] {f : α β} :
(a b c : α), a b b c (f a < f b f c < f b f b < f a f b < f c)

A function between linear orders which is neither monotone nor antitone makes a dent upright or downright.

theorem not_monotone_not_antitone_iff_exists_lt_lt {α : Type u} {β : Type v} [linear_order α] [linear_order β] {f : α β} :
(a b c : α), a < b b < c (f a < f b f c < f b f b < f a f b < f c)

A function between linear orders which is neither monotone nor antitone makes a dent upright or downright.

### Strictly monotone functions and `cmp`#

theorem strict_mono_on.cmp_map_eq {α : Type u} {β : Type v} [linear_order α] [linear_order β] {f : α β} {s : set α} {x y : α} (hf : s) (hx : x s) (hy : y s) :
cmp (f x) (f y) = cmp x y
theorem strict_mono.cmp_map_eq {α : Type u} {β : Type v} [linear_order α] [linear_order β] {f : α β} (hf : strict_mono f) (x y : α) :
cmp (f x) (f y) = cmp x y
theorem strict_anti_on.cmp_map_eq {α : Type u} {β : Type v} [linear_order α] [linear_order β] {f : α β} {s : set α} {x y : α} (hf : s) (hx : x s) (hy : y s) :
cmp (f x) (f y) = cmp y x
theorem strict_anti.cmp_map_eq {α : Type u} {β : Type v} [linear_order α] [linear_order β] {f : α β} (hf : strict_anti f) (x y : α) :
cmp (f x) (f y) = cmp y x

### Monotonicity in `ℕ` and `ℤ`#

theorem nat.rel_of_forall_rel_succ_of_le_of_lt {β : Type v} (r : β β Prop) [ r] {f : β} {a : } (h : (n : ), a n r (f n) (f (n + 1))) ⦃b c : (hab : a b) (hbc : b < c) :
r (f b) (f c)
theorem nat.rel_of_forall_rel_succ_of_le_of_le {β : Type v} (r : β β Prop) [ r] [ r] {f : β} {a : } (h : (n : ), a n r (f n) (f (n + 1))) ⦃b c : (hab : a b) (hbc : b c) :
r (f b) (f c)
theorem nat.rel_of_forall_rel_succ_of_lt {β : Type v} (r : β β Prop) [ r] {f : β} (h : (n : ), r (f n) (f (n + 1))) ⦃a b : (hab : a < b) :
r (f a) (f b)
theorem nat.rel_of_forall_rel_succ_of_le {β : Type v} (r : β β Prop) [ r] [ r] {f : β} (h : (n : ), r (f n) (f (n + 1))) ⦃a b : (hab : a b) :
r (f a) (f b)
theorem monotone_nat_of_le_succ {α : Type u} [preorder α] {f : α} (hf : (n : ), f n f (n + 1)) :
theorem antitone_nat_of_succ_le {α : Type u} [preorder α] {f : α} (hf : (n : ), f (n + 1) f n) :
theorem strict_mono_nat_of_lt_succ {α : Type u} [preorder α] {f : α} (hf : (n : ), f n < f (n + 1)) :
theorem strict_anti_nat_of_succ_lt {α : Type u} [preorder α] {f : α} (hf : (n : ), f (n + 1) < f n) :
theorem nat.exists_strict_mono' {α : Type u} [preorder α] [no_max_order α] (a : α) :
(f : α), f 0 = a

If `α` is a preorder with no maximal elements, then there exists a strictly monotone function `ℕ → α` with any prescribed value of `f 0`.

theorem nat.exists_strict_anti' {α : Type u} [preorder α] [no_min_order α] (a : α) :
(f : α), f 0 = a

If `α` is a preorder with no maximal elements, then there exists a strictly antitone function `ℕ → α` with any prescribed value of `f 0`.

theorem nat.exists_strict_mono (α : Type u) [preorder α] [nonempty α] [no_max_order α] :
(f : α),

If `α` is a nonempty preorder with no maximal elements, then there exists a strictly monotone function `ℕ → α`.

theorem nat.exists_strict_anti (α : Type u) [preorder α] [nonempty α] [no_min_order α] :
(f : α),

If `α` is a nonempty preorder with no minimal elements, then there exists a strictly antitone function `ℕ → α`.

theorem int.rel_of_forall_rel_succ_of_lt {β : Type v} (r : β β Prop) [ r] {f : β} (h : (n : ), r (f n) (f (n + 1))) ⦃a b : (hab : a < b) :
r (f a) (f b)
theorem int.rel_of_forall_rel_succ_of_le {β : Type v} (r : β β Prop) [ r] [ r] {f : β} (h : (n : ), r (f n) (f (n + 1))) ⦃a b : (hab : a b) :
r (f a) (f b)
theorem monotone_int_of_le_succ {α : Type u} [preorder α] {f : α} (hf : (n : ), f n f (n + 1)) :
theorem antitone_int_of_succ_le {α : Type u} [preorder α] {f : α} (hf : (n : ), f (n + 1) f n) :
theorem strict_mono_int_of_lt_succ {α : Type u} [preorder α] {f : α} (hf : (n : ), f n < f (n + 1)) :
theorem strict_anti_int_of_succ_lt {α : Type u} [preorder α] {f : α} (hf : (n : ), f (n + 1) < f n) :
theorem int.exists_strict_mono (α : Type u) [preorder α] [nonempty α] [no_min_order α] [no_max_order α] :
(f : α),

If `α` is a nonempty preorder with no minimal or maximal elements, then there exists a strictly monotone function `f : ℤ → α`.

theorem int.exists_strict_anti (α : Type u) [preorder α] [nonempty α] [no_min_order α] [no_max_order α] :
(f : α),

If `α` is a nonempty preorder with no minimal or maximal elements, then there exists a strictly antitone function `f : ℤ → α`.

theorem monotone.ne_of_lt_of_lt_nat {α : Type u} [preorder α] {f : α} (hf : monotone f) (n : ) {x : α} (h1 : f n < x) (h2 : x < f (n + 1)) (a : ) :
f a x

If `f` is a monotone function from `ℕ` to a preorder such that `x` lies between `f n` and `f (n + 1)`, then `x` doesn't lie in the range of `f`.

theorem antitone.ne_of_lt_of_lt_nat {α : Type u} [preorder α] {f : α} (hf : antitone f) (n : ) {x : α} (h1 : f (n + 1) < x) (h2 : x < f n) (a : ) :
f a x

If `f` is an antitone function from `ℕ` to a preorder such that `x` lies between `f (n + 1)` and `f n`, then `x` doesn't lie in the range of `f`.

theorem monotone.ne_of_lt_of_lt_int {α : Type u} [preorder α] {f : α} (hf : monotone f) (n : ) {x : α} (h1 : f n < x) (h2 : x < f (n + 1)) (a : ) :
f a x

If `f` is a monotone function from `ℤ` to a preorder and `x` lies between `f n` and `f (n + 1)`, then `x` doesn't lie in the range of `f`.

theorem antitone.ne_of_lt_of_lt_int {α : Type u} [preorder α] {f : α} (hf : antitone f) (n : ) {x : α} (h1 : f (n + 1) < x) (h2 : x < f n) (a : ) :
f a x

If `f` is an antitone function from `ℤ` to a preorder and `x` lies between `f (n + 1)` and `f n`, then `x` doesn't lie in the range of `f`.

theorem strict_mono.id_le {φ : } (h : strict_mono φ) (n : ) :
n φ n
theorem subtype.mono_coe {α : Type u} [preorder α] (t : set α) :
theorem subtype.strict_mono_coe {α : Type u} [preorder α] (t : set α) :
theorem monotone_fst {α : Type u} {β : Type v} [preorder α] [preorder β] :
theorem monotone_snd {α : Type u} {β : Type v} [preorder α] [preorder β] :
theorem monotone.prod_map {α : Type u} {β : Type v} {γ : Type w} {δ : Type u_1} [preorder α] [preorder β] [preorder γ] [preorder δ] {f : α γ} {g : β δ} (hf : monotone f) (hg : monotone g) :
theorem antitone.prod_map {α : Type u} {β : Type v} {γ : Type w} {δ : Type u_1} [preorder α] [preorder β] [preorder γ] [preorder δ] {f : α γ} {g : β δ} (hf : antitone f) (hg : antitone g) :
theorem strict_mono.prod_map {α : Type u} {β : Type v} {γ : Type w} {δ : Type u_1} [preorder γ] [preorder δ] {f : α γ} {g : β δ} (hf : strict_mono f) (hg : strict_mono g) :
theorem strict_anti.prod_map {α : Type u} {β : Type v} {γ : Type w} {δ : Type u_1} [preorder γ] [preorder δ] {f : α γ} {g : β δ} (hf : strict_anti f) (hg : strict_anti g) :
theorem function.const_mono {α : Type u} {β : Type v} [preorder α] :
theorem function.const_strict_mono {α : Type u} {β : Type v} [preorder α] [nonempty β] :