mathlib documentation

order.monotone

Monotonicity #

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 #

Main theorems #

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 α along with another typeclass we don't yet have roughly stating "everything is reachable using finitely many succ".

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
def antitone {α : Type u} {β : Type v} [preorder α] [preorder β] (f : α → β) :
Prop

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

Equations
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.

@[protected]
theorem monotone.dual {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (hf : monotone f) :
@[protected]
theorem monotone.dual_left {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (hf : monotone f) :
@[protected]
theorem monotone.dual_right {α : 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 antitone.dual_left {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (hf : antitone f) :
@[protected]
theorem antitone.dual_right {α : 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 : monotone_on f s) :
@[protected]
theorem monotone_on.dual_left {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} {s : set α} (hf : monotone_on f s) :
@[protected]
theorem monotone_on.dual_right {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} {s : set α} (hf : monotone_on f s) :
@[protected]
theorem antitone_on.dual {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} {s : set α} (hf : antitone_on f s) :
@[protected]
theorem antitone_on.dual_left {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} {s : set α} (hf : antitone_on f s) :
@[protected]
theorem antitone_on.dual_right {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} {s : set α} (hf : antitone_on f s) :
@[protected]
theorem strict_mono.dual {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (hf : strict_mono f) :
@[protected]
theorem strict_mono.dual_left {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (hf : strict_mono f) :
@[protected]
theorem strict_mono.dual_right {α : 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_anti.dual_left {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (hf : strict_anti f) :
@[protected]
theorem strict_anti.dual_right {α : 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 : strict_mono_on f s) :
@[protected]
theorem strict_mono_on.dual_left {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} {s : set α} (hf : strict_mono_on f s) :
@[protected]
theorem strict_mono_on.dual_right {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} {s : set α} (hf : strict_mono_on f s) :
@[protected]
theorem strict_anti_on.dual {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} {s : set α} (hf : strict_anti_on f s) :
@[protected]
theorem strict_anti_on.dual_left {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} {s : set α} (hf : strict_anti_on f s) :
@[protected]
theorem strict_anti_on.dual_right {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} {s : set α} (hf : strict_anti_on f s) :

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 #

@[protected]
theorem monotone.monotone_on {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (hf : monotone f) (s : set α) :
@[protected]
theorem antitone.antitone_on {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (hf : antitone f) (s : set α) :
theorem monotone_on_univ {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} :
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 α) :
theorem strict_mono_on_univ {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} :
theorem strict_anti_on_univ {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} :
theorem monotone.strict_mono_of_injective {α : Type u} {β : Type v} [preorder α] [partial_order β] {f : α → β} (h₁ : monotone f) (h₂ : function.injective f) :
theorem antitone.strict_anti_of_injective {α : Type u} {β : Type v} [preorder α] [partial_order β] {f : α → β} (h₁ : antitone f) (h₂ : function.injective f) :
@[protected]
theorem strict_mono.monotone {α : Type u} {β : Type v} [partial_order α] [preorder β] {f : α → β} (hf : strict_mono f) :
@[protected]
theorem strict_anti.antitone {α : Type u} {β : Type v} [partial_order α] [preorder β] {f : α → β} (hf : strict_anti f) :

Miscellaneous monotonicity results #

theorem monotone_id {α : Type u} [preorder α] :
theorem strict_mono_id {α : Type u} [preorder α] :
theorem monotone_const {α : Type u} {β : Type v} [preorder α] [preorder β] {c : β} :
monotone (λ (a : α), c)
theorem antitone_const {α : Type u} {β : Type v} [preorder α] [preorder β] {c : β} :
antitone (λ (a : α), c)
theorem strict_mono_of_le_iff_le {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (h : ∀ (x y : α), x y f x f y) :
theorem injective_of_lt_imp_ne {α : Type u} {β : Type v} [linear_order α] {f : α → β} (h : ∀ (x y : α), x < yf x f y) :
theorem injective_of_le_imp_le {α : Type u} {β : Type v} [partial_order α] [preorder β] (f : α → β) (h : ∀ {x y : α}, f x f yx y) :
@[protected]
theorem strict_mono.ite' {α : Type u} {β : Type v} [preorder α] [preorder β] {f g : α → β} (hf : strict_mono f) (hg : strict_mono g) {p : α → Prop} [decidable_pred p] (hp : ∀ ⦃x y : α⦄, x < yp yp x) (hfg : ∀ ⦃x y : α⦄, p x¬p yx < yf 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} [decidable_pred p] (hp : ∀ ⦃x y : α⦄, x < yp yp 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} [decidable_pred p] (hp : ∀ ⦃x y : α⦄, x < yp yp x) (hfg : ∀ ⦃x y : α⦄, p x¬p yx < yg 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} [decidable_pred p] (hp : ∀ ⦃x y : α⦄, x < yp yp 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 : monotone_on f s) :
theorem monotone.comp_antitone_on {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder β] [preorder γ] {g : β → γ} {f : α → β} {s : set α} (hg : monotone g) (hf : antitone_on f s) :
@[protected]
theorem antitone.comp_antitone_on {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder β] [preorder γ] {g : β → γ} {f : α → β} {s : set α} (hg : antitone g) (hf : antitone_on f s) :
theorem antitone.comp_monotone_on {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder β] [preorder γ] {g : β → γ} {f : α → β} {s : set α} (hg : antitone g) (hf : monotone_on f 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 : strict_mono_on f 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 : strict_anti_on f 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 : strict_anti_on f 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 : strict_mono_on f s) :

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 strict_mono_on.le_iff_le {α : Type u} {β : Type v} [linear_order α] [preorder β] {f : α → β} {s : set α} (hf : strict_mono_on f 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 : strict_anti_on f 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 : strict_mono_on f 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 : strict_anti_on f 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 : strict_mono_on f 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 : strict_anti_on f 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 α] [partial_order β] {f : α → β} (hf : monotone f) :
theorem antitone.strict_anti_iff_injective {α : Type u} {β : Type v} [linear_order α] [partial_order β] {f : α → β} (hf : antitone f) :

Monotonicity in and #

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 v} [preorder β] {f : → β} (hf : ∀ (n : ), f n < f (n + 1)) :
theorem strict_anti_nat_of_succ_lt {β : Type v} [preorder β] {f : → β} (hf : ∀ (n : ), f (n + 1) < f n) :
theorem forall_ge_le_of_forall_le_succ {α : Type u} [preorder α] (f : → α) {a : } (h : ∀ (n : ), a nf n.succ f n) {b c : } (hab : a b) (hbc : b c) :
f c f b
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_1} {β : Type u_2} [preorder α] [preorder β] :
theorem monotone_snd {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] :