Documentation

Mathlib.Order.Monotone.Basic

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.
MonotoneOn f s: Same as Monotone f, but for all a, b ∈ s.
AntitoneOn f s: Same as Antitone f, but for all a, b ∈ s.
StrictMono f : A function f between two preorders is strictly monotone if a < b implies f a < f b.
StrictAnti f : A function f between two preorders is strictly antitone if a < b implies f b < f a.
StrictMonoOn f s: Same as StrictMono f, but for all a, b ∈ s.
StrictAntiOn f s: Same as StrictAnti 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.
strictMono_nat_of_lt_succ, strictMono_int_of_lt_succ: If f : ℕ → α or f : ℤ → α and f n < f (n + 1) for all n, then f is strictly monotone.
strictAnti_nat_of_succ_lt, strictAnti_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 LE α or 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 SuccOrder α and IsSuccArchimedean α.

Tags #

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

def Monotone {α : Type u} {β : Type v} [Preorder α] [Preorder β] (f : α → β) :

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

Equations

Monotone f = ∀ ⦃a b : α⦄, a ≤ b → f a ≤ f b

Instances For

def Antitone {α : Type u} {β : Type v} [Preorder α] [Preorder β] (f : α → β) :

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

Equations

Antitone f = ∀ ⦃a b : α⦄, a ≤ b → f b ≤ f a

Instances For

def MonotoneOn {α : Type u} {β : Type v} [Preorder α] [Preorder β] (f : α → β) (s : Set α) :

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

Equations

MonotoneOn f s = ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → a ≤ b → f a ≤ f b

Instances For

def AntitoneOn {α : Type u} {β : Type v} [Preorder α] [Preorder β] (f : α → β) (s : Set α) :

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

Equations

AntitoneOn f s = ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → a ≤ b → f b ≤ f a

Instances For

def StrictMono {α : Type u} {β : Type v} [Preorder α] [Preorder β] (f : α → β) :

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

Equations

StrictMono f = ∀ ⦃a b : α⦄, a < b → f a < f b

Instances For

def StrictAnti {α : Type u} {β : Type v} [Preorder α] [Preorder β] (f : α → β) :

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

Equations

StrictAnti f = ∀ ⦃a b : α⦄, a < b → f b < f a

Instances For

def StrictMonoOn {α : Type u} {β : Type v} [Preorder α] [Preorder β] (f : α → β) (s : Set α) :

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

Equations

StrictMonoOn f s = ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → a < b → f a < f b

Instances For

def StrictAntiOn {α : Type u} {β : Type v} [Preorder α] [Preorder β] (f : α → β) (s : Set α) :

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

Equations

StrictAntiOn f s = ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → a < b → f b < f a

Instances For

instance instDecidableMonotoneOfForallForallForallLe {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} [i : Decidable (∀ (a b : α), a ≤ b → f a ≤ f b)] :

Decidable (Monotone f)

Equations

instDecidableMonotoneOfForallForallForallLe = i

instance instDecidableAntitoneOfForallForallForallLe {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} [i : Decidable (∀ (a b : α), a ≤ b → f b ≤ f a)] :

Decidable (Antitone f)

Equations

instDecidableAntitoneOfForallForallForallLe = i

instance instDecidableMonotoneOnOfForallForallMemSetForallForallForallLe {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} [i : Decidable (∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a ≤ b → f a ≤ f b)] :

Decidable (MonotoneOn f s)

Equations

instDecidableMonotoneOnOfForallForallMemSetForallForallForallLe = i

instance instDecidableAntitoneOnOfForallForallMemSetForallForallForallLe {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} [i : Decidable (∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a ≤ b → f b ≤ f a)] :

Decidable (AntitoneOn f s)

Equations

instDecidableAntitoneOnOfForallForallMemSetForallForallForallLe = i

instance instDecidableStrictMonoOfForallForallForallLt {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} [i : Decidable (∀ (a b : α), a < b → f a < f b)] :

Decidable (StrictMono f)

Equations

instDecidableStrictMonoOfForallForallForallLt = i

instance instDecidableStrictAntiOfForallForallForallLt {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} [i : Decidable (∀ (a b : α), a < b → f b < f a)] :

Decidable (StrictAnti f)

Equations

instDecidableStrictAntiOfForallForallForallLt = i

instance instDecidableStrictMonoOnOfForallForallMemSetForallForallForallLt {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} [i : Decidable (∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a < b → f a < f b)] :

Decidable (StrictMonoOn f s)

Equations

instDecidableStrictMonoOnOfForallForallMemSetForallForallForallLt = i

instance instDecidableStrictAntiOnOfForallForallMemSetForallForallForallLt {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} [i : Decidable (∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a < b → f b < f a)] :

Decidable (StrictAntiOn f s)

Equations

instDecidableStrictAntiOnOfForallForallMemSetForallForallForallLt = i

theorem monotone_inclusion_le_le_of_le {α : Type u} [Preorder α] {k j : α} (hkj : k ≤ j) :

Monotone fun (x : { i : α // i ≤ k }) => match x with | ⟨i, hi⟩ => ⟨i, ⋯⟩

theorem monotone_inclusion_lt_le_of_le {α : Type u} [Preorder α] {k j : α} (hkj : k ≤ j) :

Monotone fun (x : { i : α // i < k }) => match x with | ⟨i, hi⟩ => ⟨i, ⋯⟩

theorem monotone_inclusion_lt_lt_of_le {α : Type u} [Preorder α] {k j : α} (hkj : k ≤ j) :

Monotone fun (x : { i : α // i < k }) => match x with | ⟨i, hi⟩ => ⟨i, ⋯⟩

Monotonicity on the dual order #

Strictly, many of the *On.dual lemmas in this section should use ofDual ⁻¹' 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_ofDual_iff {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} :

Monotone (f ∘ ⇑OrderDual.ofDual) ↔ Antitone f

@[simp]

theorem antitone_comp_ofDual_iff {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} :

Antitone (f ∘ ⇑OrderDual.ofDual) ↔ Monotone f

@[simp]

theorem monotone_toDual_comp_iff {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} :

Monotone (⇑OrderDual.toDual ∘ f) ↔ Antitone f

@[simp]

theorem antitone_toDual_comp_iff {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} :

Antitone (⇑OrderDual.toDual ∘ f) ↔ Monotone f

@[simp]

theorem monotoneOn_comp_ofDual_iff {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} :

MonotoneOn (f ∘ ⇑OrderDual.ofDual) s ↔ AntitoneOn f s

@[simp]

theorem antitoneOn_comp_ofDual_iff {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} :

AntitoneOn (f ∘ ⇑OrderDual.ofDual) s ↔ MonotoneOn f s

@[simp]

theorem monotoneOn_toDual_comp_iff {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} :

MonotoneOn (⇑OrderDual.toDual ∘ f) s ↔ AntitoneOn f s

@[simp]

theorem antitoneOn_toDual_comp_iff {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} :

AntitoneOn (⇑OrderDual.toDual ∘ f) s ↔ MonotoneOn f s

@[simp]

theorem strictMono_comp_ofDual_iff {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} :

StrictMono (f ∘ ⇑OrderDual.ofDual) ↔ StrictAnti f

@[simp]

theorem strictAnti_comp_ofDual_iff {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} :

StrictAnti (f ∘ ⇑OrderDual.ofDual) ↔ StrictMono f

@[simp]

theorem strictMono_toDual_comp_iff {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} :

StrictMono (⇑OrderDual.toDual ∘ f) ↔ StrictAnti f

@[simp]

theorem strictAnti_toDual_comp_iff {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} :

StrictAnti (⇑OrderDual.toDual ∘ f) ↔ StrictMono f

@[simp]

theorem strictMonoOn_comp_ofDual_iff {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} :

StrictMonoOn (f ∘ ⇑OrderDual.ofDual) s ↔ StrictAntiOn f s

@[simp]

theorem strictAntiOn_comp_ofDual_iff {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} :

StrictAntiOn (f ∘ ⇑OrderDual.ofDual) s ↔ StrictMonoOn f s

@[simp]

theorem strictMonoOn_toDual_comp_iff {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} :

StrictMonoOn (⇑OrderDual.toDual ∘ f) s ↔ StrictAntiOn f s

@[simp]

theorem strictAntiOn_toDual_comp_iff {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} :

StrictAntiOn (⇑OrderDual.toDual ∘ f) s ↔ StrictMonoOn f s

theorem monotone_dual_iff {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} :

Monotone (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual) ↔ Monotone f

theorem antitone_dual_iff {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} :

Antitone (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual) ↔ Antitone f

theorem monotoneOn_dual_iff {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} :

MonotoneOn (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual) s ↔ MonotoneOn f s

theorem antitoneOn_dual_iff {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} :

AntitoneOn (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual) s ↔ AntitoneOn f s

theorem strictMono_dual_iff {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} :

StrictMono (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual) ↔ StrictMono f

theorem strictAnti_dual_iff {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} :

StrictAnti (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual) ↔ StrictAnti f

theorem strictMonoOn_dual_iff {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} :

StrictMonoOn (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual) s ↔ StrictMonoOn f s

theorem strictAntiOn_dual_iff {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} :

StrictAntiOn (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual) s ↔ StrictAntiOn f s

theorem Monotone.dual_left {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} :

Monotone f → Antitone (f ∘ ⇑OrderDual.ofDual)

Alias of the reverse direction of antitone_comp_ofDual_iff.

theorem Antitone.dual_left {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} :

Antitone f → Monotone (f ∘ ⇑OrderDual.ofDual)

Alias of the reverse direction of monotone_comp_ofDual_iff.

theorem Monotone.dual_right {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} :

Monotone f → Antitone (⇑OrderDual.toDual ∘ f)

Alias of the reverse direction of antitone_toDual_comp_iff.

theorem Antitone.dual_right {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} :

Antitone f → Monotone (⇑OrderDual.toDual ∘ f)

Alias of the reverse direction of monotone_toDual_comp_iff.

theorem MonotoneOn.dual_left {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} :

MonotoneOn f s → AntitoneOn (f ∘ ⇑OrderDual.ofDual) s

Alias of the reverse direction of antitoneOn_comp_ofDual_iff.

theorem AntitoneOn.dual_left {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} :

AntitoneOn f s → MonotoneOn (f ∘ ⇑OrderDual.ofDual) s

Alias of the reverse direction of monotoneOn_comp_ofDual_iff.

theorem MonotoneOn.dual_right {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} :

MonotoneOn f s → AntitoneOn (⇑OrderDual.toDual ∘ f) s

Alias of the reverse direction of antitoneOn_toDual_comp_iff.

theorem AntitoneOn.dual_right {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} :

AntitoneOn f s → MonotoneOn (⇑OrderDual.toDual ∘ f) s

Alias of the reverse direction of monotoneOn_toDual_comp_iff.

theorem StrictMono.dual_left {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} :

StrictMono f → StrictAnti (f ∘ ⇑OrderDual.ofDual)

Alias of the reverse direction of strictAnti_comp_ofDual_iff.

theorem StrictAnti.dual_left {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} :

StrictAnti f → StrictMono (f ∘ ⇑OrderDual.ofDual)

Alias of the reverse direction of strictMono_comp_ofDual_iff.

theorem StrictMono.dual_right {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} :

StrictMono f → StrictAnti (⇑OrderDual.toDual ∘ f)

Alias of the reverse direction of strictAnti_toDual_comp_iff.

theorem StrictAnti.dual_right {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} :

StrictAnti f → StrictMono (⇑OrderDual.toDual ∘ f)

Alias of the reverse direction of strictMono_toDual_comp_iff.

theorem StrictMonoOn.dual_left {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} :

StrictMonoOn f s → StrictAntiOn (f ∘ ⇑OrderDual.ofDual) s

Alias of the reverse direction of strictAntiOn_comp_ofDual_iff.

theorem StrictAntiOn.dual_left {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} :

StrictAntiOn f s → StrictMonoOn (f ∘ ⇑OrderDual.ofDual) s

Alias of the reverse direction of strictMonoOn_comp_ofDual_iff.

theorem StrictMonoOn.dual_right {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} :

StrictMonoOn f s → StrictAntiOn (⇑OrderDual.toDual ∘ f) s

Alias of the reverse direction of strictAntiOn_toDual_comp_iff.

theorem StrictAntiOn.dual_right {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} :

StrictAntiOn f s → StrictMonoOn (⇑OrderDual.toDual ∘ f) s

Alias of the reverse direction of strictMonoOn_toDual_comp_iff.

theorem Monotone.dual {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} :

Monotone f → Monotone (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual)

Alias of the reverse direction of monotone_dual_iff.

theorem Antitone.dual {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} :

Antitone f → Antitone (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual)

Alias of the reverse direction of antitone_dual_iff.

theorem MonotoneOn.dual {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} :

MonotoneOn f s → MonotoneOn (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual) s

Alias of the reverse direction of monotoneOn_dual_iff.

theorem AntitoneOn.dual {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} :

AntitoneOn f s → AntitoneOn (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual) s

Alias of the reverse direction of antitoneOn_dual_iff.

theorem StrictMono.dual {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} :

StrictMono f → StrictMono (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual)

Alias of the reverse direction of strictMono_dual_iff.

theorem StrictAnti.dual {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} :

StrictAnti f → StrictAnti (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual)

Alias of the reverse direction of strictAnti_dual_iff.

theorem StrictMonoOn.dual {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} :

StrictMonoOn f s → StrictMonoOn (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual) s

Alias of the reverse direction of strictMonoOn_dual_iff.

theorem StrictAntiOn.dual {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} :

StrictAntiOn f s → StrictAntiOn (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual) s

Alias of the reverse direction of strictAntiOn_dual_iff.

theorem StrictMono.wellFoundedLT {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} [WellFoundedLT β] (hf : StrictMono f) :

WellFoundedLT α

theorem StrictAnti.wellFoundedLT {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} [WellFoundedGT β] (hf : StrictAnti f) :

WellFoundedLT α

theorem StrictMono.wellFoundedGT {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} [WellFoundedGT β] (hf : StrictMono f) :

WellFoundedGT α

theorem StrictAnti.wellFoundedGT {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} [WellFoundedLT β] (hf : StrictAnti f) :

WellFoundedGT α

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 fun (a : α) => f a b) :

theorem monotone_app {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder γ] (f : β → α → γ) (b : β) (hf : Monotone fun (a : α) (b : β) => f b a) :

theorem antitone_lam {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder γ] {f : α → β → γ} (hf : ∀ (b : β), Antitone fun (a : α) => f a b) :

theorem antitone_app {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder γ] (f : β → α → γ) (b : β) (hf : Antitone fun (a : α) (b : β) => f b a) :

theorem Function.monotone_eval {ι : Type u} {α : ι → Type v} [(i : ι) → Preorder (α i)] (i : ι) :

Monotone (Function.eval 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 StrictMono.imp {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {a b : α} (hf : StrictMono f) (h : a < b) :

f a < f b

theorem StrictAnti.imp {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {a b : α} (hf : StrictAnti f) (h : a < b) :

f b < f a

theorem Monotone.monotoneOn {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} (hf : Monotone f) (s : Set α) :

theorem Antitone.antitoneOn {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} (hf : Antitone f) (s : Set α) :

@[simp]

theorem monotoneOn_univ {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} :

MonotoneOn f Set.univ ↔ Monotone f

@[simp]

theorem antitoneOn_univ {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} :

AntitoneOn f Set.univ ↔ Antitone f

theorem StrictMono.strictMonoOn {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} (hf : StrictMono f) (s : Set α) :

StrictMonoOn f s

theorem StrictAnti.strictAntiOn {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} (hf : StrictAnti f) (s : Set α) :

StrictAntiOn f s

@[simp]

theorem strictMonoOn_univ {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} :

StrictMonoOn f Set.univ ↔ StrictMono f

@[simp]

theorem strictAntiOn_univ {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} :

StrictAntiOn f Set.univ ↔ StrictAnti f

theorem Monotone.strictMono_of_injective {α : Type u} {β : Type v} [Preorder α] [PartialOrder β] {f : α → β} (h₁ : Monotone f) (h₂ : Function.Injective f) :

theorem Antitone.strictAnti_of_injective {α : Type u} {β : Type v} [Preorder α] [PartialOrder β] {f : α → β} (h₁ : Antitone f) (h₂ : Function.Injective f) :

theorem monotone_iff_forall_lt {α : Type u} {β : Type v} [PartialOrder α] [Preorder β] {f : α → β} :

Monotone f ↔ ∀ ⦃a b : α⦄, a < b → f a ≤ f b

theorem antitone_iff_forall_lt {α : Type u} {β : Type v} [PartialOrder α] [Preorder β] {f : α → β} :

Antitone f ↔ ∀ ⦃a b : α⦄, a < b → f b ≤ f a

theorem monotoneOn_iff_forall_lt {α : Type u} {β : Type v} [PartialOrder α] [Preorder β] {f : α → β} {s : Set α} :

MonotoneOn f s ↔ ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → a < b → f a ≤ f b

theorem antitoneOn_iff_forall_lt {α : Type u} {β : Type v} [PartialOrder α] [Preorder β] {f : α → β} {s : Set α} :

AntitoneOn f s ↔ ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → a < b → f b ≤ f a

theorem StrictMonoOn.monotoneOn {α : Type u} {β : Type v} [PartialOrder α] [Preorder β] {f : α → β} {s : Set α} (hf : StrictMonoOn f s) :

theorem StrictAntiOn.antitoneOn {α : Type u} {β : Type v} [PartialOrder α] [Preorder β] {f : α → β} {s : Set α} (hf : StrictAntiOn f s) :

theorem StrictMono.monotone {α : Type u} {β : Type v} [PartialOrder α] [Preorder β] {f : α → β} (hf : StrictMono f) :

theorem StrictAnti.antitone {α : Type u} {β : Type v} [PartialOrder α] [Preorder β] {f : α → β} (hf : StrictAnti f) :

Monotonicity from and to subsingletons #

theorem Subsingleton.monotone {α : Type u} {β : Type v} [Preorder α] [Preorder β] [Subsingleton α] (f : α → β) :

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 : α → β) :

theorem Subsingleton.strictMono {α : Type u} {β : Type v} [Preorder α] [Preorder β] [Subsingleton α] (f : α → β) :

theorem Subsingleton.strictAnti {α : Type u} {β : Type v} [Preorder α] [Preorder β] [Subsingleton α] (f : α → β) :

Miscellaneous monotonicity results #

theorem monotone_id {α : Type u} [Preorder α] :

theorem monotoneOn_id {α : Type u} [Preorder α] {s : Set α} :

MonotoneOn id s

theorem strictMono_id {α : Type u} [Preorder α] :

theorem strictMonoOn_id {α : Type u} [Preorder α] {s : Set α} :

StrictMonoOn id s

theorem monotone_const {α : Type u} {β : Type v} [Preorder α] [Preorder β] {c : β} :

Monotone fun (x : α) => c

theorem monotoneOn_const {α : Type u} {β : Type v} [Preorder α] [Preorder β] {c : β} {s : Set α} :

MonotoneOn (fun (x : α) => c) s

theorem antitone_const {α : Type u} {β : Type v} [Preorder α] [Preorder β] {c : β} :

Antitone fun (x : α) => c

theorem antitoneOn_const {α : Type u} {β : Type v} [Preorder α] [Preorder β] {c : β} {s : Set α} :

AntitoneOn (fun (x : α) => c) s

theorem strictMono_of_le_iff_le {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} (h : ∀ (x y : α), x ≤ y ↔ f x ≤ f y) :

theorem strictAnti_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} [LinearOrder α] {f : α → β} (h : ∀ (x y : α), x < y → f x ≠ f y) :

Function.Injective f

theorem injective_of_le_imp_le {α : Type u} {β : Type v} [PartialOrder α] [Preorder β] (f : α → β) (h : ∀ {x y : α}, f x ≤ f y → x ≤ y) :

Function.Injective f

theorem StrictMono.isMax_of_apply {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {a : α} (hf : StrictMono f) (ha : IsMax (f a)) :

theorem StrictMono.isMin_of_apply {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {a : α} (hf : StrictMono f) (ha : IsMin (f a)) :

theorem StrictAnti.isMax_of_apply {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {a : α} (hf : StrictAnti f) (ha : IsMin (f a)) :

theorem StrictAnti.isMin_of_apply {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {a : α} (hf : StrictAnti f) (ha : IsMax (f a)) :

theorem StrictMono.add_le_nat {f : ℕ → ℕ} (hf : StrictMono f) (m n : ℕ) :

m + f n ≤ f (m + n)

theorem StrictMono.ite' {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f g : α → β} (hf : StrictMono f) (hg : StrictMono g) {p : α → Prop} [DecidablePred p] (hp : ∀ ⦃x y : α⦄, x < y → p y → p x) (hfg : ∀ ⦃x y : α⦄, p x → ¬p y → x < y → f x < g y) :

StrictMono fun (x : α) => if p x then f x else g x

theorem StrictMono.ite {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f g : α → β} (hf : StrictMono f) (hg : StrictMono g) {p : α → Prop} [DecidablePred p] (hp : ∀ ⦃x y : α⦄, x < y → p y → p x) (hfg : ∀ (x : α), f x ≤ g x) :

StrictMono fun (x : α) => if p x then f x else g x

theorem StrictAnti.ite' {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f g : α → β} (hf : StrictAnti f) (hg : StrictAnti g) {p : α → Prop} [DecidablePred p] (hp : ∀ ⦃x y : α⦄, x < y → p y → p x) (hfg : ∀ ⦃x y : α⦄, p x → ¬p y → x < y → g y < f x) :

StrictAnti fun (x : α) => if p x then f x else g x

theorem StrictAnti.ite {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f g : α → β} (hf : StrictAnti f) (hg : StrictAnti g) {p : α → Prop} [DecidablePred p] (hp : ∀ ⦃x y : α⦄, x < y → p y → p x) (hfg : ∀ (x : α), g x ≤ f x) :

StrictAnti fun (x : α) => if p x then f x else g x

Monotonicity under composition #

theorem Monotone.comp {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {g : β → γ} {f : α → β} (hg : Monotone g) (hf : Monotone f) :

Monotone (g ∘ f)

theorem Monotone.comp_antitone {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {g : β → γ} {f : α → β} (hg : Monotone g) (hf : Antitone f) :

Antitone (g ∘ f)

theorem Antitone.comp {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {g : β → γ} {f : α → β} (hg : Antitone g) (hf : Antitone f) :

Monotone (g ∘ f)

theorem Antitone.comp_monotone {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {g : β → γ} {f : α → β} (hg : Antitone g) (hf : Monotone f) :

Antitone (g ∘ f)

theorem Monotone.iterate {α : Type u} [Preorder α] {f : α → α} (hf : Monotone f) (n : ℕ) :

theorem Monotone.comp_monotoneOn {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {g : β → γ} {f : α → β} {s : Set α} (hg : Monotone g) (hf : MonotoneOn f s) :

MonotoneOn (g ∘ f) s

theorem Monotone.comp_antitoneOn {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {g : β → γ} {f : α → β} {s : Set α} (hg : Monotone g) (hf : AntitoneOn f s) :

AntitoneOn (g ∘ f) s

theorem Antitone.comp_antitoneOn {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {g : β → γ} {f : α → β} {s : Set α} (hg : Antitone g) (hf : AntitoneOn f s) :

MonotoneOn (g ∘ f) s

theorem Antitone.comp_monotoneOn {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {g : β → γ} {f : α → β} {s : Set α} (hg : Antitone g) (hf : MonotoneOn f s) :

AntitoneOn (g ∘ f) s

theorem StrictMono.comp {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {g : β → γ} {f : α → β} (hg : StrictMono g) (hf : StrictMono f) :

StrictMono (g ∘ f)

theorem StrictMono.comp_strictAnti {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {g : β → γ} {f : α → β} (hg : StrictMono g) (hf : StrictAnti f) :

StrictAnti (g ∘ f)

theorem StrictAnti.comp {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {g : β → γ} {f : α → β} (hg : StrictAnti g) (hf : StrictAnti f) :

StrictMono (g ∘ f)

theorem StrictAnti.comp_strictMono {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {g : β → γ} {f : α → β} (hg : StrictAnti g) (hf : StrictMono f) :

StrictAnti (g ∘ f)

theorem StrictMono.iterate {α : Type u} [Preorder α] {f : α → α} (hf : StrictMono f) (n : ℕ) :

StrictMono f^[n]

theorem StrictMono.comp_strictMonoOn {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {g : β → γ} {f : α → β} {s : Set α} (hg : StrictMono g) (hf : StrictMonoOn f s) :

StrictMonoOn (g ∘ f) s

theorem StrictMono.comp_strictAntiOn {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {g : β → γ} {f : α → β} {s : Set α} (hg : StrictMono g) (hf : StrictAntiOn f s) :

StrictAntiOn (g ∘ f) s

theorem StrictAnti.comp_strictAntiOn {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {g : β → γ} {f : α → β} {s : Set α} (hg : StrictAnti g) (hf : StrictAntiOn f s) :

StrictMonoOn (g ∘ f) s

theorem StrictAnti.comp_strictMonoOn {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {g : β → γ} {f : α → β} {s : Set α} (hg : StrictAnti g) (hf : StrictMonoOn f s) :

StrictAntiOn (g ∘ f) s

theorem List.foldl_monotone {α : Type u} {β : Type v} [Preorder α] {f : α → β → α} (H : ∀ (b : β), Monotone fun (a : α) => f a b) (l : List β) :

Monotone fun (a : α) => List.foldl f a l

theorem List.foldr_monotone {α : Type u} {β : Type v} [Preorder β] {f : α → β → β} (H : ∀ (a : α), Monotone (f a)) (l : List α) :

Monotone fun (b : β) => List.foldr f b l

theorem List.foldl_strictMono {α : Type u} {β : Type v} [Preorder α] {f : α → β → α} (H : ∀ (b : β), StrictMono fun (a : α) => f a b) (l : List β) :

StrictMono fun (a : α) => List.foldl f a l

theorem List.foldr_strictMono {α : Type u} {β : Type v} [Preorder β] {f : α → β → β} (H : ∀ (a : α), StrictMono (f a)) (l : List α) :

StrictMono fun (b : β) => List.foldr f b l

Monotonicity in linear orders #

theorem Monotone.reflect_lt {α : Type u} {β : Type v} [LinearOrder α] [Preorder β] {f : α → β} (hf : Monotone f) {a b : α} (h : f a < f b) :

a < b

theorem Antitone.reflect_lt {α : Type u} {β : Type v} [LinearOrder α] [Preorder β] {f : α → β} (hf : Antitone f) {a b : α} (h : f a < f b) :

b < a

theorem MonotoneOn.reflect_lt {α : Type u} {β : Type v} [LinearOrder α] [Preorder β] {f : α → β} {s : Set α} (hf : MonotoneOn f s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) (h : f a < f b) :

a < b

theorem AntitoneOn.reflect_lt {α : Type u} {β : Type v} [LinearOrder α] [Preorder β] {f : α → β} {s : Set α} (hf : AntitoneOn f s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) (h : f a < f b) :

b < a

theorem StrictMonoOn.le_iff_le {α : Type u} {β : Type v} [LinearOrder α] [Preorder β] {f : α → β} {s : Set α} (hf : StrictMonoOn f s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) :

f a ≤ f b ↔ a ≤ b

theorem StrictAntiOn.le_iff_le {α : Type u} {β : Type v} [LinearOrder α] [Preorder β] {f : α → β} {s : Set α} (hf : StrictAntiOn f s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) :

f a ≤ f b ↔ b ≤ a

theorem StrictMonoOn.eq_iff_eq {α : Type u} {β : Type v} [LinearOrder α] [Preorder β] {f : α → β} {s : Set α} (hf : StrictMonoOn f s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) :

f a = f b ↔ a = b

theorem StrictAntiOn.eq_iff_eq {α : Type u} {β : Type v} [LinearOrder α] [Preorder β] {f : α → β} {s : Set α} (hf : StrictAntiOn f s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) :

f a = f b ↔ b = a

theorem StrictMonoOn.lt_iff_lt {α : Type u} {β : Type v} [LinearOrder α] [Preorder β] {f : α → β} {s : Set α} (hf : StrictMonoOn f s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) :

f a < f b ↔ a < b

theorem StrictAntiOn.lt_iff_lt {α : Type u} {β : Type v} [LinearOrder α] [Preorder β] {f : α → β} {s : Set α} (hf : StrictAntiOn f s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) :

f a < f b ↔ b < a

theorem StrictMono.le_iff_le {α : Type u} {β : Type v} [LinearOrder α] [Preorder β] {f : α → β} (hf : StrictMono f) {a b : α} :

f a ≤ f b ↔ a ≤ b

theorem StrictAnti.le_iff_le {α : Type u} {β : Type v} [LinearOrder α] [Preorder β] {f : α → β} (hf : StrictAnti f) {a b : α} :

f a ≤ f b ↔ b ≤ a

theorem StrictMono.lt_iff_lt {α : Type u} {β : Type v} [LinearOrder α] [Preorder β] {f : α → β} (hf : StrictMono f) {a b : α} :

f a < f b ↔ a < b

theorem StrictAnti.lt_iff_lt {α : Type u} {β : Type v} [LinearOrder α] [Preorder β] {f : α → β} (hf : StrictAnti f) {a b : α} :

f a < f b ↔ b < a

theorem StrictMonoOn.compares {α : Type u} {β : Type v} [LinearOrder α] [Preorder β] {f : α → β} {s : Set α} (hf : StrictMonoOn f s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) {o : Ordering} :

o.Compares (f a) (f b) ↔ o.Compares a b

theorem StrictAntiOn.compares {α : Type u} {β : Type v} [LinearOrder α] [Preorder β] {f : α → β} {s : Set α} (hf : StrictAntiOn f s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) {o : Ordering} :

o.Compares (f a) (f b) ↔ o.Compares b a

theorem StrictMono.compares {α : Type u} {β : Type v} [LinearOrder α] [Preorder β] {f : α → β} (hf : StrictMono f) {a b : α} {o : Ordering} :

o.Compares (f a) (f b) ↔ o.Compares a b

theorem StrictAnti.compares {α : Type u} {β : Type v} [LinearOrder α] [Preorder β] {f : α → β} (hf : StrictAnti f) {a b : α} {o : Ordering} :

o.Compares (f a) (f b) ↔ o.Compares b a

theorem StrictMono.injective {α : Type u} {β : Type v} [LinearOrder α] [Preorder β] {f : α → β} (hf : StrictMono f) :

Function.Injective f

theorem StrictAnti.injective {α : Type u} {β : Type v} [LinearOrder α] [Preorder β] {f : α → β} (hf : StrictAnti f) :

Function.Injective f

theorem StrictMono.maximal_of_maximal_image {α : Type u} {β : Type v} [LinearOrder α] [Preorder β] {f : α → β} (hf : StrictMono f) {a : α} (hmax : ∀ (p : β), p ≤ f a) (x : α) :

x ≤ a

theorem StrictMono.minimal_of_minimal_image {α : Type u} {β : Type v} [LinearOrder α] [Preorder β] {f : α → β} (hf : StrictMono f) {a : α} (hmin : ∀ (p : β), f a ≤ p) (x : α) :

a ≤ x

theorem StrictAnti.minimal_of_maximal_image {α : Type u} {β : Type v} [LinearOrder α] [Preorder β] {f : α → β} (hf : StrictAnti f) {a : α} (hmax : ∀ (p : β), p ≤ f a) (x : α) :

a ≤ x

theorem StrictAnti.maximal_of_minimal_image {α : Type u} {β : Type v} [LinearOrder α] [Preorder β] {f : α → β} (hf : StrictAnti f) {a : α} (hmin : ∀ (p : β), f a ≤ p) (x : α) :

x ≤ a

theorem Monotone.strictMono_iff_injective {α : Type u} {β : Type v} [LinearOrder α] [PartialOrder β] {f : α → β} (hf : Monotone f) :

StrictMono f ↔ Function.Injective f

theorem Antitone.strictAnti_iff_injective {α : Type u} {β : Type v} [LinearOrder α] [PartialOrder β] {f : α → β} (hf : Antitone f) :

StrictAnti f ↔ Function.Injective f

theorem Monotone.eq_of_le_of_le {α : Type u} {β : Type v} [LinearOrder α] [PartialOrder β] {f : α → β} {a₁ a₂ : α} (h_mon : Monotone f) (h_fa : f a₁ = f a₂) {i : α} (h₁ : a₁ ≤ i) (h₂ : i ≤ a₂) :

f i = f a₁

If a monotone function is equal at two points, it is equal between all of them

theorem Antitone.eq_of_le_of_le {α : Type u} {β : Type v} [LinearOrder α] [PartialOrder β] {f : α → β} {a₁ a₂ : α} (h_anti : Antitone f) (h_fa : f a₁ = f a₂) {i : α} (h₁ : a₁ ≤ i) (h₂ : i ≤ a₂) :

f i = f a₁

If an antitone function is equal at two points, it is equal between all of them

theorem not_monotone_not_antitone_iff_exists_le_le {α : Type u} {β : Type v} [LinearOrder α] [LinearOrder β] {f : α → β} :

¬Monotone f ∧ ¬Antitone 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} [LinearOrder α] [LinearOrder β] {f : α → β} :

¬Monotone f ∧ ¬Antitone 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 StrictMonoOn.cmp_map_eq {α : Type u} {β : Type v} [LinearOrder α] [LinearOrder β] {f : α → β} {s : Set α} {x y : α} (hf : StrictMonoOn f s) (hx : x ∈ s) (hy : y ∈ s) :

cmp (f x) (f y) = cmp x y

theorem StrictMono.cmp_map_eq {α : Type u} {β : Type v} [LinearOrder α] [LinearOrder β] {f : α → β} (hf : StrictMono f) (x y : α) :

cmp (f x) (f y) = cmp x y

theorem StrictAntiOn.cmp_map_eq {α : Type u} {β : Type v} [LinearOrder α] [LinearOrder β] {f : α → β} {s : Set α} {x y : α} (hf : StrictAntiOn f s) (hx : x ∈ s) (hy : y ∈ s) :

cmp (f x) (f y) = cmp y x

theorem StrictAnti.cmp_map_eq {α : Type u} {β : Type v} [LinearOrder α] [LinearOrder β] {f : α → β} (hf : StrictAnti 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) [IsTrans β 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) [IsRefl β r] [IsTrans β 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) [IsTrans β 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) [IsRefl β r] [IsTrans β 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 strictMono_nat_of_lt_succ {α : Type u} [Preorder α] {f : ℕ → α} (hf : ∀ (n : ℕ), f n < f (n + 1)) :

theorem strictAnti_nat_of_succ_lt {α : Type u} [Preorder α] {f : ℕ → α} (hf : ∀ (n : ℕ), f (n + 1) < f n) :

theorem Nat.exists_strictMono' {α : Type u} [Preorder α] [NoMaxOrder α] (a : α) :

∃ (f : ℕ → α), StrictMono 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_strictAnti' {α : Type u} [Preorder α] [NoMinOrder α] (a : α) :

∃ (f : ℕ → α), StrictAnti 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_strictMono (α : Type u) [Preorder α] [Nonempty α] [NoMaxOrder α] :

∃ (f : ℕ → α), StrictMono f

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

theorem Nat.exists_strictAnti (α : Type u) [Preorder α] [Nonempty α] [NoMinOrder α] :

∃ (f : ℕ → α), StrictAnti 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) [IsTrans β 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) [IsRefl β r] [IsTrans β 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 strictMono_int_of_lt_succ {α : Type u} [Preorder α] {f : ℤ → α} (hf : ∀ (n : ℤ), f n < f (n + 1)) :

theorem strictAnti_int_of_succ_lt {α : Type u} [Preorder α] {f : ℤ → α} (hf : ∀ (n : ℤ), f (n + 1) < f n) :

theorem Int.exists_strictMono (α : Type u) [Preorder α] [Nonempty α] [NoMinOrder α] [NoMaxOrder α] :

∃ (f : ℤ → α), StrictMono f

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

theorem Int.exists_strictAnti (α : Type u) [Preorder α] [Nonempty α] [NoMinOrder α] [NoMaxOrder α] :

∃ (f : ℤ → α), StrictAnti 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 Subtype.mono_coe {α : Type u} [Preorder α] (t : Set α) :

Monotone Subtype.val

theorem Subtype.strictMono_coe {α : Type u} [Preorder α] (t : Set α) :

StrictMono Subtype.val

theorem monotone_fst {α : Type u} {β : Type v} [Preorder α] [Preorder β] :

Monotone Prod.fst

theorem monotone_snd {α : Type u} {β : Type v} [Preorder α] [Preorder β] :

Monotone Prod.snd

theorem Monotone.prod_map {α : Type u} {β : Type v} {γ : Type w} {δ : Type u_2} [Preorder α] [Preorder β] [Preorder γ] [Preorder δ] {f : α → γ} {g : β → δ} (hf : Monotone f) (hg : Monotone g) :

Monotone (Prod.map f g)

theorem Antitone.prod_map {α : Type u} {β : Type v} {γ : Type w} {δ : Type u_2} [Preorder α] [Preorder β] [Preorder γ] [Preorder δ] {f : α → γ} {g : β → δ} (hf : Antitone f) (hg : Antitone g) :

Antitone (Prod.map f g)

theorem StrictMono.prod_map {α : Type u} {β : Type v} {γ : Type w} {δ : Type u_2} [PartialOrder α] [PartialOrder β] [Preorder γ] [Preorder δ] {f : α → γ} {g : β → δ} (hf : StrictMono f) (hg : StrictMono g) :

StrictMono (Prod.map f g)

theorem StrictAnti.prod_map {α : Type u} {β : Type v} {γ : Type w} {δ : Type u_2} [PartialOrder α] [PartialOrder β] [Preorder γ] [Preorder δ] {f : α → γ} {g : β → δ} (hf : StrictAnti f) (hg : StrictAnti g) :

StrictAnti (Prod.map f g)

Pi types #

theorem Function.update_mono {ι : Type u_1} {π : ι → Type u_3} [DecidableEq ι] [(i : ι) → Preorder (π i)] {f : (i : ι) → π i} {i : ι} :

Monotone (Function.update f i)

theorem Function.update_strictMono {ι : Type u_1} {π : ι → Type u_3} [DecidableEq ι] [(i : ι) → Preorder (π i)] {f : (i : ι) → π i} {i : ι} :

StrictMono (Function.update f i)

theorem Function.const_mono {α : Type u} {β : Type v} [Preorder α] :

Monotone (Function.const β)

theorem Function.const_strictMono {α : Type u} {β : Type v} [Preorder α] [Nonempty β] :

StrictMono (Function.const β)

theorem monotone_iff_apply₂ {ι : Type u_1} {α : Type u} {β : ι → Type u_4} [(i : ι) → Preorder (β i)] [Preorder α] {f : α → (i : ι) → β i} :

Monotone f ↔ ∀ (i : ι), Monotone fun (x : α) => f x i

theorem antitone_iff_apply₂ {ι : Type u_1} {α : Type u} {β : ι → Type u_4} [(i : ι) → Preorder (β i)] [Preorder α] {f : α → (i : ι) → β i} :

Antitone f ↔ ∀ (i : ι), Antitone fun (x : α) => f x i

theorem Monotone.of_apply₂ {ι : Type u_1} {α : Type u} {β : ι → Type u_4} [(i : ι) → Preorder (β i)] [Preorder α] {f : α → (i : ι) → β i} :

(∀ (i : ι), Monotone fun (x : α) => f x i) → Monotone f

Alias of the reverse direction of monotone_iff_apply₂.

theorem Monotone.apply₂ {ι : Type u_1} {α : Type u} {β : ι → Type u_4} [(i : ι) → Preorder (β i)] [Preorder α] {f : α → (i : ι) → β i} :

Monotone f → ∀ (i : ι), Monotone fun (x : α) => f x i

Alias of the forward direction of monotone_iff_apply₂.

theorem Antitone.of_apply₂ {ι : Type u_1} {α : Type u} {β : ι → Type u_4} [(i : ι) → Preorder (β i)] [Preorder α] {f : α → (i : ι) → β i} :

(∀ (i : ι), Antitone fun (x : α) => f x i) → Antitone f

Alias of the reverse direction of antitone_iff_apply₂.

theorem Antitone.apply₂ {ι : Type u_1} {α : Type u} {β : ι → Type u_4} [(i : ι) → Preorder (β i)] [Preorder α] {f : α → (i : ι) → β i} :

Antitone f → ∀ (i : ι), Antitone fun (x : α) => f x i

Alias of the forward direction of antitone_iff_apply₂.

theorem Nat.stabilises_of_monotone {f : ℕ → ℕ} {b n : ℕ} (hfmono : Monotone f) (hfb : ∀ (m : ℕ), f m ≤ b) (hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)) (hbn : b ≤ n) :

f n = f b

A monotone function f : ℕ → ℕ bounded by b, which is constant after stabilising for the first time, stabilises in at most b steps.

theorem Nat.stabilises_of_monotone.strictMono {f : ℕ → ℕ} {b : ℕ} (hfmono : Monotone f) (hfb : ∀ (m : ℕ), m ≤ b → f m ≠ f (m + 1)) (m : ℕ) :

m ≤ b + 1 → m ≤ f m

@[deprecated Nat.stabilises_of_monotone]

theorem Group.card_pow_eq_card_pow_card_univ_aux {f : ℕ → ℕ} {b n : ℕ} (hfmono : Monotone f) (hfb : ∀ (m : ℕ), f m ≤ b) (hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)) (hbn : b ≤ n) :

f n = f b

Alias of Nat.stabilises_of_monotone.

A monotone function f : ℕ → ℕ bounded by b, which is constant after stabilising for the first time, stabilises in at most b steps.

@[deprecated Nat.stabilises_of_monotone]

theorem Group.card_nsmul_eq_card_nsmulpow_card_univ_aux {f : ℕ → ℕ} {b n : ℕ} (hfmono : Monotone f) (hfb : ∀ (m : ℕ), f m ≤ b) (hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)) (hbn : b ≤ n) :

f n = f b

Alias of Nat.stabilises_of_monotone.

A monotone function f : ℕ → ℕ bounded by b, which is constant after stabilising for the first time, stabilises in at most b steps.