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 #

• 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
• = ∀ ⦃a b : α⦄, a bf a f b
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
• = ∀ ⦃a b : α⦄, a bf b f a
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
• s = ∀ ⦃a : α⦄, a s∀ ⦃b : α⦄, b sa bf a f b
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
• s = ∀ ⦃a : α⦄, a s∀ ⦃b : α⦄, b sa bf b f a
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
• = ∀ ⦃a b : α⦄, a < bf a < f b
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
• = ∀ ⦃a b : α⦄, a < bf b < f a
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
• = ∀ ⦃a : α⦄, a s∀ ⦃b : α⦄, b sa < bf a < f b
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
• = ∀ ⦃a : α⦄, a s∀ ⦃b : α⦄, b sa < bf b < f a

### 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
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 α] {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 < bf a f b
theorem antitone_iff_forall_lt {α : Type u} {β : Type v} [preorder β] {f : α → β} :
∀ ⦃a b : α⦄, a < bf b f a
theorem monotone_on_iff_forall_lt {α : Type u} {β : Type v} [preorder β] {f : α → β} {s : set α} :
s ∀ ⦃a : α⦄, a s∀ ⦃b : α⦄, b sa < bf a f b
theorem antitone_on_iff_forall_lt {α : Type u} {β : Type v} [preorder β] {f : α → β} {s : set α} :
s ∀ ⦃a : α⦄, a s∀ ⦃b : α⦄, b sa < bf 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 < yf x f y) :
theorem injective_of_le_imp_le {α : Type u} {β : Type v} [preorder β] (f : α → β) (h : ∀ {x y : α}, f x f yx 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 < 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} (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} (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} (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 : 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.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) :

### 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 nr (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 nr (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) :