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

source

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

Prop

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

Equations

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

source

def antitone {α : Type u} {β : Type v} [preorder α] [preorder β] (f : α → β) :

Prop

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

Equations

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

strict_anti_on f s = ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → a < b → f 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.

source

@[protected]

theorem monotone.dual {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (hf : monotone f) :

monotone (⇑order_dual.to_dual ∘ f ∘ ⇑order_dual.of_dual)

source

@[protected]

theorem monotone.dual_left {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (hf : monotone f) :

antitone (f ∘ ⇑order_dual.of_dual)

source

@[protected]

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

antitone (⇑order_dual.to_dual ∘ f)

source

@[protected]

theorem antitone.dual {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (hf : antitone f) :

antitone (⇑order_dual.to_dual ∘ f ∘ ⇑order_dual.of_dual)

source

@[protected]

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

monotone (f ∘ ⇑order_dual.of_dual)

source

@[protected]

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

monotone (⇑order_dual.to_dual ∘ f)

source

@[protected]

theorem monotone_on.dual {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} {s : set α} (hf : monotone_on f s) :

monotone_on (⇑order_dual.to_dual ∘ f ∘ ⇑order_dual.of_dual) s

source

@[protected]

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

antitone_on (f ∘ ⇑order_dual.of_dual) s

source

@[protected]

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

antitone_on (⇑order_dual.to_dual ∘ f) s

source

@[protected]

theorem antitone_on.dual {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} {s : set α} (hf : antitone_on f s) :

antitone_on (⇑order_dual.to_dual ∘ f ∘ ⇑order_dual.of_dual) s

source

@[protected]

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

monotone_on (f ∘ ⇑order_dual.of_dual) s

source

@[protected]

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

monotone_on (⇑order_dual.to_dual ∘ f) s

source

@[protected]

theorem strict_mono.dual {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (hf : strict_mono f) :

strict_mono (⇑order_dual.to_dual ∘ f ∘ ⇑order_dual.of_dual)

source

@[protected]

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

strict_anti (f ∘ ⇑order_dual.of_dual)

source

@[protected]

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

strict_anti (⇑order_dual.to_dual ∘ f)

source

@[protected]

theorem strict_anti.dual {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (hf : strict_anti f) :

strict_anti (⇑order_dual.to_dual ∘ f ∘ ⇑order_dual.of_dual)

source

@[protected]

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

strict_mono (f ∘ ⇑order_dual.of_dual)

source

@[protected]

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

strict_mono (⇑order_dual.to_dual ∘ f)

source

@[protected]

theorem strict_mono_on.dual {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} {s : set α} (hf : strict_mono_on f s) :

strict_mono_on (⇑order_dual.to_dual ∘ f ∘ ⇑order_dual.of_dual) s

source

@[protected]

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

strict_anti_on (f ∘ ⇑order_dual.of_dual) s

source

@[protected]

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

strict_anti_on (⇑order_dual.to_dual ∘ f) s

source

@[protected]

theorem strict_anti_on.dual {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} {s : set α} (hf : strict_anti_on f s) :

strict_anti_on (⇑order_dual.to_dual ∘ f ∘ ⇑order_dual.of_dual) s

source

@[protected]

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

strict_mono_on (f ∘ ⇑order_dual.of_dual) s

source

@[protected]

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

strict_mono_on (⇑order_dual.to_dual ∘ f) s

Monotonicity in function spaces #

source

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

source

theorem monotone_lam {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder γ] {f : α → β → γ} (hf : ∀ (b : β), monotone (λ (a : α), f a b)) :

monotone f

source

theorem monotone_app {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder γ] (f : β → α → γ) (b : β) (hf : monotone (λ (a : α) (b : β), f b a)) :

monotone (f b)

source

theorem antitone_lam {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder γ] {f : α → β → γ} (hf : ∀ (b : β), antitone (λ (a : α), f a b)) :

antitone f

source

theorem antitone_app {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder γ] (f : β → α → γ) (b : β) (hf : antitone (λ (a : α) (b : β), f b a)) :

antitone (f b)

source

theorem function.monotone_eval {ι : Type u} {α : ι → Type v} [Π (i : ι), preorder (α i)] (i : ι) :

monotone (function.eval i)

Monotonicity hierarchy #

source

@[protected]

theorem monotone.monotone_on {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (hf : monotone f) (s : set α) :

monotone_on f s

source

@[protected]

theorem antitone.antitone_on {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (hf : antitone f) (s : set α) :

antitone_on f s

source

theorem monotone_on_univ {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} :

monotone_on f set.univ ↔ monotone f

source

theorem antitone_on_univ {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} :

antitone_on f set.univ ↔ antitone f

source

@[protected]

theorem strict_mono.strict_mono_on {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (hf : strict_mono f) (s : set α) :

strict_mono_on f s

source

@[protected]

theorem strict_anti.strict_anti_on {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (hf : strict_anti f) (s : set α) :

strict_anti_on f s

source

theorem strict_mono_on_univ {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} :

strict_mono_on f set.univ ↔ strict_mono f

source

theorem strict_anti_on_univ {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} :

strict_anti_on f set.univ ↔ strict_anti f

source

theorem monotone.strict_mono_of_injective {α : Type u} {β : Type v} [preorder α] [partial_order β] {f : α → β} (h₁ : monotone f) (h₂ : function.injective f) :

strict_mono f

source

theorem antitone.strict_anti_of_injective {α : Type u} {β : Type v} [preorder α] [partial_order β] {f : α → β} (h₁ : antitone f) (h₂ : function.injective f) :

strict_anti f

source

theorem monotone_iff_forall_lt {α : Type u} {β : Type v} [partial_order α] [preorder β] {f : α → β} :

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

source

theorem antitone_iff_forall_lt {α : Type u} {β : Type v} [partial_order α] [preorder β] {f : α → β} :

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

source

theorem monotone_on_iff_forall_lt {α : Type u} {β : Type v} [partial_order α] [preorder β] {f : α → β} {s : set α} :

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

source

theorem antitone_on_iff_forall_lt {α : Type u} {β : Type v} [partial_order α] [preorder β] {f : α → β} {s : set α} :

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

source

@[protected]

theorem strict_mono_on.monotone_on {α : Type u} {β : Type v} [partial_order α] [preorder β] {f : α → β} {s : set α} (hf : strict_mono_on f s) :

monotone_on f s

source

@[protected]

theorem strict_anti_on.antitone_on {α : Type u} {β : Type v} [partial_order α] [preorder β] {f : α → β} {s : set α} (hf : strict_anti_on f s) :

antitone_on f s

source

@[protected]

theorem strict_mono.monotone {α : Type u} {β : Type v} [partial_order α] [preorder β] {f : α → β} (hf : strict_mono f) :

monotone f

source

@[protected]

theorem strict_anti.antitone {α : Type u} {β : Type v} [partial_order α] [preorder β] {f : α → β} (hf : strict_anti f) :

antitone f

Monotonicity from and to subsingletons #

source

@[protected]

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

monotone f

source

@[protected]

theorem subsingleton.antitone {α : Type u} {β : Type v} [preorder α] [preorder β] [subsingleton α] (f : α → β) :

antitone f

source

theorem subsingleton.monotone' {α : Type u} {β : Type v} [preorder α] [preorder β] [subsingleton β] (f : α → β) :

monotone f

source

theorem subsingleton.antitone' {α : Type u} {β : Type v} [preorder α] [preorder β] [subsingleton β] (f : α → β) :

antitone f

source

@[protected]

theorem subsingleton.strict_mono {α : Type u} {β : Type v} [preorder α] [preorder β] [subsingleton α] (f : α → β) :

strict_mono f

source

@[protected]

theorem subsingleton.strict_anti {α : Type u} {β : Type v} [preorder α] [preorder β] [subsingleton α] (f : α → β) :

strict_anti f

Miscellaneous monotonicity results #

source

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

monotone id

source

theorem strict_mono_id {α : Type u} [preorder α] :

strict_mono id

source

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

monotone (λ (a : α), c)

source

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

antitone (λ (a : α), c)

source

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

strict_mono f

source

theorem injective_of_lt_imp_ne {α : Type u} {β : Type v} [linear_order α] {f : α → β} (h : ∀ (x y : α), x < y → f x ≠ f y) :

function.injective f

source

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

function.injective f

source

@[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 < y → p y → p x) (hfg : ∀ ⦃x y : α⦄, p x → ¬p y → x < y → f x < g y) :

strict_mono (λ (x : α), ite (p x) (f x) (g x))

source

@[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 < y → p y → p x) (hfg : ∀ (x : α), f x ≤ g x) :

strict_mono (λ (x : α), ite (p x) (f x) (g x))

source

@[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 < y → p y → p x) (hfg : ∀ ⦃x y : α⦄, p x → ¬p y → x < y → g y < f x) :

strict_anti (λ (x : α), ite (p x) (f x) (g x))

source

@[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 < y → p y → p x) (hfg : ∀ (x : α), g x ≤ f x) :

strict_anti (λ (x : α), ite (p x) (f x) (g x))

Monotonicity under composition #

source

@[protected]

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

monotone (g ∘ f)

source

theorem monotone.comp_antitone {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder β] [preorder γ] {g : β → γ} {f : α → β} (hg : monotone g) (hf : antitone f) :

antitone (g ∘ f)

source

@[protected]

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

monotone (g ∘ f)

source

theorem antitone.comp_monotone {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder β] [preorder γ] {g : β → γ} {f : α → β} (hg : antitone g) (hf : monotone f) :

antitone (g ∘ f)

source

@[protected]

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

monotone f^[n]

source

@[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) :

monotone_on (g ∘ f) s

source

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) :

antitone_on (g ∘ f) s

source

@[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) :

monotone_on (g ∘ f) s

source

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) :

antitone_on (g ∘ f) s

source

@[protected]

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

strict_mono (g ∘ f)

source

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) :

strict_anti (g ∘ f)

source

@[protected]

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

strict_mono (g ∘ f)

source

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) :

strict_anti (g ∘ f)

source

@[protected]

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

strict_mono f^[n]

source

@[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) :

strict_mono_on (g ∘ f) s

source

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) :

strict_anti_on (g ∘ f) s

source

@[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) :

strict_mono_on (g ∘ f) s

source

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) :

strict_anti_on (g ∘ f) s

Monotonicity in linear orders #

source

theorem monotone.reflect_lt {α : Type u} {β : Type v} [linear_order α] [preorder β] {f : α → β} (hf : monotone f) {a b : α} (h : f a < f b) :

a < b

source

theorem antitone.reflect_lt {α : Type u} {β : Type v} [linear_order α] [preorder β] {f : α → β} (hf : antitone f) {a b : α} (h : f a < f b) :

b < a

source

theorem monotone_on.reflect_lt {α : Type u} {β : Type v} [linear_order α] [preorder β] {f : α → β} {s : set α} (hf : monotone_on f s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) (h : f a < f b) :

a < b

source

theorem antitone_on.reflect_lt {α : Type u} {β : Type v} [linear_order α] [preorder β] {f : α → β} {s : set α} (hf : antitone_on f s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) (h : f a < f b) :

b < a

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

@[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

source

@[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

source

@[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

source

@[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

source

theorem strict_mono.injective {α : Type u} {β : Type v} [linear_order α] [preorder β] {f : α → β} (hf : strict_mono f) :

function.injective f

source

theorem strict_anti.injective {α : Type u} {β : Type v} [linear_order α] [preorder β] {f : α → β} (hf : strict_anti f) :

function.injective f

source

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

source

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

source

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

source

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

source

theorem monotone.strict_mono_iff_injective {α : Type u} {β : Type v} [linear_order α] [partial_order β] {f : α → β} (hf : monotone f) :

strict_mono f ↔ function.injective f

source

theorem antitone.strict_anti_iff_injective {α : Type u} {β : Type v} [linear_order α] [partial_order β] {f : α → β} (hf : antitone f) :

strict_anti f ↔ function.injective f

Monotonicity in `ℕ` and `ℤ` #

source

theorem nat.rel_of_forall_rel_succ_of_le_of_lt {β : Type v} (r : β → β → Prop) [is_trans β 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)

source

theorem nat.rel_of_forall_rel_succ_of_le_of_le {β : Type v} (r : β → β → Prop) [is_refl β r] [is_trans β 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)

source

theorem nat.rel_of_forall_rel_succ_of_lt {β : Type v} (r : β → β → Prop) [is_trans β r] {f : ℕ → β} (h : ∀ (n : ℕ), r (f n) (f (n + 1))) ⦃a b : ℕ⦄ (hab : a < b) :

r (f a) (f b)

source

theorem nat.rel_of_forall_rel_succ_of_le {β : Type v} (r : β → β → Prop) [is_refl β r] [is_trans β r] {f : ℕ → β} (h : ∀ (n : ℕ), r (f n) (f (n + 1))) ⦃a b : ℕ⦄ (hab : a ≤ b) :

r (f a) (f b)

source

theorem monotone_nat_of_le_succ {α : Type u} [preorder α] {f : ℕ → α} (hf : ∀ (n : ℕ), f n ≤ f (n + 1)) :

monotone f

source

theorem antitone_nat_of_succ_le {α : Type u} [preorder α] {f : ℕ → α} (hf : ∀ (n : ℕ), f (n + 1) ≤ f n) :

antitone f

source

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

strict_mono f

source

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

strict_anti f

source

theorem int.rel_of_forall_rel_succ_of_lt {β : Type v} (r : β → β → Prop) [is_trans β r] {f : ℤ → β} (h : ∀ (n : ℤ), r (f n) (f (n + 1))) ⦃a b : ℤ⦄ (hab : a < b) :

r (f a) (f b)

source

theorem int.rel_of_forall_rel_succ_of_le {β : Type v} (r : β → β → Prop) [is_refl β r] [is_trans β r] {f : ℤ → β} (h : ∀ (n : ℤ), r (f n) (f (n + 1))) ⦃a b : ℤ⦄ (hab : a ≤ b) :

r (f a) (f b)

source

theorem monotone_int_of_le_succ {α : Type u} [preorder α] {f : ℤ → α} (hf : ∀ (n : ℤ), f n ≤ f (n + 1)) :

monotone f

source

theorem antitone_int_of_succ_le {α : Type u} [preorder α] {f : ℤ → α} (hf : ∀ (n : ℤ), f (n + 1) ≤ f n) :

antitone f

source

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

strict_mono f

source

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

strict_anti f

source

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.

source

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.

source

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.

source

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.

source