Monotonicity #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file defines (strictly) monotone/antitone functions. Contrary to standard mathematical usage, "monotone"/"mono" here means "increasing", not "increasing or decreasing". We use "antitone"/"anti" to mean "decreasing".
Definitions #
monotone f: A functionfbetween two preorders is monotone ifa ≤ bimpliesf a ≤ f b.antitone f: A functionfbetween two preorders is antitone ifa ≤ bimpliesf b ≤ f a.monotone_on f s: Same asmonotone f, but for alla, b ∈ s.antitone_on f s: Same asantitone f, but for alla, b ∈ s.strict_mono f: A functionfbetween two preorders is strictly monotone ifa < bimpliesf a < f b.strict_anti f: A functionfbetween two preorders is strictly antitone ifa < bimpliesf b < f a.strict_mono_on f s: Same asstrict_mono f, but for alla, b ∈ s.strict_anti_on f s: Same asstrict_anti f, but for alla, b ∈ s.
Main theorems #
monotone_nat_of_le_succ,monotone_int_of_le_succ: Iff : ℕ → αorf : ℤ → αandf n ≤ f (n + 1)for alln, thenfis monotone.antitone_nat_of_succ_le,antitone_int_of_succ_le: Iff : ℕ → αorf : ℤ → αandf (n + 1) ≤ f nfor alln, thenfis antitone.strict_mono_nat_of_lt_succ,strict_mono_int_of_lt_succ: Iff : ℕ → αorf : ℤ → αandf n < f (n + 1)for alln, thenfis strictly monotone.strict_anti_nat_of_succ_lt,strict_anti_int_of_succ_lt: Iff : ℕ → αorf : ℤ → αandf (n + 1) < f nfor alln, thenfis 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
A function f is monotone on s if, for all a, b ∈ s, a ≤ b implies f a ≤ f b.
Instances for monotone_on
A function f is antitone on s if, for all a, b ∈ s, a ≤ b implies f b ≤ f a.
Instances for antitone_on
A function f is strictly monotone if a < b implies f a < f b.
Instances for strict_mono
A function f is strictly antitone if a < b implies f b < f a.
Instances for strict_anti
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_on_comp_of_dual_iff
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
{f : α → β}
{s : set α} :
monotone_on (f ∘ ⇑order_dual.of_dual) s ↔ antitone_on f s
@[simp]
theorem
antitone_on_comp_of_dual_iff
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
{f : α → β}
{s : set α} :
antitone_on (f ∘ ⇑order_dual.of_dual) s ↔ monotone_on f s
@[simp]
theorem
monotone_on_to_dual_comp_iff
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
{f : α → β}
{s : set α} :
monotone_on (⇑order_dual.to_dual ∘ f) s ↔ antitone_on f s
@[simp]
theorem
antitone_on_to_dual_comp_iff
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
{f : α → β}
{s : set α} :
antitone_on (⇑order_dual.to_dual ∘ f) s ↔ monotone_on f s
@[simp]
theorem
strict_mono_on_comp_of_dual_iff
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
{f : α → β}
{s : set α} :
strict_mono_on (f ∘ ⇑order_dual.of_dual) s ↔ strict_anti_on f s
@[simp]
theorem
strict_anti_on_comp_of_dual_iff
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
{f : α → β}
{s : set α} :
strict_anti_on (f ∘ ⇑order_dual.of_dual) s ↔ strict_mono_on f s
@[simp]
theorem
strict_mono_on_to_dual_comp_iff
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
{f : α → β}
{s : set α} :
strict_mono_on (⇑order_dual.to_dual ∘ f) s ↔ strict_anti_on f s
@[simp]
theorem
strict_anti_on_to_dual_comp_iff
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
{f : α → β}
{s : set α} :
strict_anti_on (⇑order_dual.to_dual ∘ f) s ↔ strict_mono_on f s
@[protected]
theorem
monotone_on.dual
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
{f : α → β}
{s : set α}
(hf : monotone_on f s) :
@[protected]
theorem
antitone_on.dual
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
{f : α → β}
{s : set α}
(hf : antitone_on f s) :
@[protected]
theorem
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 : strict_mono_on f s) :
@[protected]
theorem
strict_anti_on.dual
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
{f : α → β}
{s : set α}
(hf : strict_anti_on f s) :
Alias of the reverse direction of antitone_comp_of_dual_iff.
Alias of the reverse direction of monotone_comp_of_dual_iff.
Alias of the reverse direction of antitone_to_dual_comp_iff.
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 α} :
monotone_on f s → antitone_on (f ∘ ⇑order_dual.of_dual) 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 α} :
antitone_on f s → monotone_on (f ∘ ⇑order_dual.of_dual) 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 α} :
monotone_on f s → antitone_on (⇑order_dual.to_dual ∘ f) 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 α} :
antitone_on f s → monotone_on (⇑order_dual.to_dual ∘ f) s
Alias of the reverse direction of monotone_on_to_dual_comp_iff.
Alias of the reverse direction of strict_anti_comp_of_dual_iff.
Alias of the reverse direction of strict_mono_comp_of_dual_iff.
Alias of the reverse direction of strict_anti_to_dual_comp_iff.
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 α} :
strict_mono_on f s → strict_anti_on (f ∘ ⇑order_dual.of_dual) s
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 α} :
strict_anti_on f s → strict_mono_on (f ∘ ⇑order_dual.of_dual) s
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 α} :
strict_mono_on f s → strict_anti_on (⇑order_dual.to_dual ∘ f) s
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 α} :
strict_anti_on f s → strict_mono_on (⇑order_dual.to_dual ∘ f) s
Alias of the reverse direction of strict_mono_on_to_dual_comp_iff.
Monotonicity in function spaces #
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
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 α) :
monotone_on f s
@[protected]
theorem
antitone.antitone_on
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
{f : α → β}
(hf : antitone f)
(s : set α) :
antitone_on f s
@[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
@[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
theorem
monotone.strict_mono_of_injective
{α : Type u}
{β : Type v}
[preorder α]
[partial_order β]
{f : α → β}
(h₁ : monotone f)
(h₂ : function.injective f) :
theorem
antitone.strict_anti_of_injective
{α : Type u}
{β : Type v}
[preorder α]
[partial_order β]
{f : α → β}
(h₁ : antitone f)
(h₂ : function.injective f) :
@[protected]
theorem
strict_mono_on.monotone_on
{α : Type u}
{β : Type v}
[partial_order α]
[preorder β]
{f : α → β}
{s : set α}
(hf : strict_mono_on f s) :
monotone_on f s
@[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
@[protected]
theorem
strict_mono.monotone
{α : Type u}
{β : Type v}
[partial_order α]
[preorder β]
{f : α → β}
(hf : strict_mono f) :
monotone f
@[protected]
theorem
strict_anti.antitone
{α : Type u}
{β : Type v}
[partial_order α]
[preorder β]
{f : α → β}
(hf : strict_anti f) :
antitone f
Monotonicity from and to subsingletons #
@[protected]
theorem
subsingleton.monotone
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
[subsingleton α]
(f : α → β) :
monotone f
@[protected]
theorem
subsingleton.antitone
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
[subsingleton α]
(f : α → β) :
antitone f
theorem
subsingleton.monotone'
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
[subsingleton β]
(f : α → β) :
monotone f
theorem
subsingleton.antitone'
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
[subsingleton β]
(f : α → β) :
antitone 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_on_const
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
{c : β}
{s : set α} :
monotone_on (λ (a : α), c) s
theorem
antitone_on_const
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
{c : β}
{s : set α} :
antitone_on (λ (a : α), c) s
theorem
injective_of_lt_imp_ne
{α : Type u}
{β : Type v}
[linear_order α]
{f : α → β}
(h : ∀ (x y : α), x < y → f x ≠ f y) :
theorem
injective_of_le_imp_le
{α : Type u}
{β : Type v}
[partial_order α]
[preorder β]
(f : α → β)
(h : ∀ {x y : α}, f x ≤ f y → x ≤ y) :
theorem
strict_mono.is_max_of_apply
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
{f : α → β}
{a : α}
(hf : strict_mono f)
(ha : is_max (f a)) :
is_max 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)) :
is_min 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)) :
is_max 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)) :
is_min a
@[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))
@[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))
@[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))
@[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 #
@[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
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
@[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
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
@[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)
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)
@[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)
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)
@[protected]
@[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
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
@[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
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
theorem
list.foldl_strict_mono
{α : Type u}
{β : Type v}
[preorder α]
{f : α → β → α}
(H : ∀ (b : β), strict_mono (λ (a : α), f a b))
(l : list β) :
strict_mono (λ (a : α), list.foldl f a l)
theorem
list.foldr_strict_mono
{α : Type u}
{β : Type v}
[preorder β]
{f : α → β → β}
(H : ∀ (a : α), strict_mono (f a))
(l : list α) :
strict_mono (λ (b : β), list.foldr f 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 : monotone_on f 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 : antitone_on f 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 : strict_mono_on f s)
{a b : α}
(ha : a ∈ s)
(hb : b ∈ s) :
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) :
theorem
strict_mono_on.eq_iff_eq
{α : Type u}
{β : Type v}
[linear_order α]
[preorder β]
{f : α → β}
{s : set α}
(hf : strict_mono_on f s)
{a b : α}
(ha : a ∈ s)
(hb : b ∈ s) :
theorem
strict_anti_on.eq_iff_eq
{α : Type u}
{β : Type v}
[linear_order α]
[preorder β]
{f : α → β}
{s : set α}
(hf : strict_anti_on f s)
{a b : α}
(ha : a ∈ s)
(hb : b ∈ s) :
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) :
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) :
theorem
strict_mono.le_iff_le
{α : Type u}
{β : Type v}
[linear_order α]
[preorder β]
{f : α → β}
(hf : strict_mono f)
{a b : α} :
theorem
strict_anti.le_iff_le
{α : Type u}
{β : Type v}
[linear_order α]
[preorder β]
{f : α → β}
(hf : strict_anti f)
{a b : α} :
theorem
strict_mono.lt_iff_lt
{α : Type u}
{β : Type v}
[linear_order α]
[preorder β]
{f : α → β}
(hf : strict_mono f)
{a b : α} :
theorem
strict_anti.lt_iff_lt
{α : Type u}
{β : Type v}
[linear_order α]
[preorder β]
{f : α → β}
(hf : strict_anti f)
{a b : α} :
@[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} :
@[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} :
@[protected]
theorem
strict_mono.compares
{α : Type u}
{β : Type v}
[linear_order α]
[preorder β]
{f : α → β}
(hf : strict_mono f)
{a b : α}
{o : ordering} :
@[protected]
theorem
strict_anti.compares
{α : Type u}
{β : Type v}
[linear_order α]
[preorder β]
{f : α → β}
(hf : strict_anti f)
{a b : α}
{o : ordering} :
theorem
strict_mono.injective
{α : Type u}
{β : Type v}
[linear_order α]
[preorder β]
{f : α → β}
(hf : strict_mono f) :
theorem
strict_anti.injective
{α : Type u}
{β : Type v}
[linear_order α]
[preorder β]
{f : α → β}
(hf : strict_anti f) :
theorem
strict_mono.maximal_of_maximal_image
{α : Type u}
{β : Type v}
[linear_order α]
[preorder β]
{f : α → β}
(hf : strict_mono f)
{a : α}
(hmax : ∀ (p : β), p ≤ f a)
(x : α) :
x ≤ a
theorem
strict_mono.minimal_of_minimal_image
{α : Type u}
{β : Type v}
[linear_order α]
[preorder β]
{f : α → β}
(hf : strict_mono f)
{a : α}
(hmin : ∀ (p : β), f a ≤ p)
(x : α) :
a ≤ x
theorem
strict_anti.minimal_of_maximal_image
{α : Type u}
{β : Type v}
[linear_order α]
[preorder β]
{f : α → β}
(hf : strict_anti f)
{a : α}
(hmax : ∀ (p : β), p ≤ f a)
(x : α) :
a ≤ x
theorem
strict_anti.maximal_of_minimal_image
{α : Type u}
{β : Type v}
[linear_order α]
[preorder β]
{f : α → β}
(hf : strict_anti f)
{a : α}
(hmin : ∀ (p : β), f a ≤ p)
(x : α) :
x ≤ a
theorem
monotone.strict_mono_iff_injective
{α : Type u}
{β : Type v}
[linear_order α]
[partial_order β]
{f : α → β}
(hf : monotone f) :
theorem
antitone.strict_anti_iff_injective
{α : Type u}
{β : Type v}
[linear_order α]
[partial_order β]
{f : α → β}
(hf : antitone f) :
theorem
not_monotone_not_antitone_iff_exists_le_le
{α : Type u}
{β : Type v}
[linear_order α]
[linear_order β]
{f : α → β} :
A function between linear orders which is neither monotone nor antitone makes a dent upright or downright.
theorem
not_monotone_not_antitone_iff_exists_lt_lt
{α : Type u}
{β : Type v}
[linear_order α]
[linear_order β]
{f : α → β} :
A function between linear orders which is neither monotone nor antitone makes a dent upright or downright.
theorem
strict_mono_on.cmp_map_eq
{α : Type u}
{β : Type v}
[linear_order α]
[linear_order β]
{f : α → β}
{s : set α}
{x y : α}
(hf : strict_mono_on f s)
(hx : x ∈ s)
(hy : y ∈ s) :
theorem
strict_mono.cmp_map_eq
{α : Type u}
{β : Type v}
[linear_order α]
[linear_order β]
{f : α → β}
(hf : strict_mono f)
(x y : α) :
theorem
strict_anti_on.cmp_map_eq
{α : Type u}
{β : Type v}
[linear_order α]
[linear_order β]
{f : α → β}
{s : set α}
{x y : α}
(hf : strict_anti_on f s)
(hx : x ∈ s)
(hy : y ∈ s) :
theorem
strict_anti.cmp_map_eq
{α : Type u}
{β : Type v}
[linear_order α]
[linear_order β]
{f : α → β}
(hf : strict_anti f)
(x y : α) :
Monotonicity in ℕ and ℤ #
If α is a preorder with no maximal elements, then there exists a strictly monotone function
ℕ → α with any prescribed value of f 0.
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 : ℕ → α), strict_mono 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 : ℕ → α), strict_anti f
If α is a nonempty preorder with no minimal elements, then there exists a strictly antitone
function ℕ → α.
theorem
int.exists_strict_mono
(α : Type u)
[preorder α]
[nonempty α]
[no_min_order α]
[no_max_order α] :
∃ (f : ℤ → α), strict_mono 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 : ℤ → α), strict_anti f
If α is a nonempty preorder with no minimal or maximal elements, then there exists a strictly
antitone function f : ℤ → α.
theorem
strict_mono.prod_map
{α : Type u}
{β : Type v}
{γ : Type w}
{δ : Type u_2}
[partial_order α]
[partial_order β]
[preorder γ]
[preorder δ]
{f : α → γ}
{g : β → δ}
(hf : strict_mono f)
(hg : strict_mono g) :
strict_mono (prod.map f g)
theorem
strict_anti.prod_map
{α : Type u}
{β : Type v}
{γ : Type w}
{δ : Type u_2}
[partial_order α]
[partial_order β]
[preorder γ]
[preorder δ]
{f : α → γ}
{g : β → δ}
(hf : strict_anti f)
(hg : strict_anti g) :
strict_anti (prod.map f g)
Pi types #
theorem
function.update_mono
{ι : Type u_1}
{π : ι → Type u_3}
[decidable_eq ι]
[Π (i : ι), preorder (π i)]
{f : Π (i : ι), π i}
{i : ι} :
monotone (function.update f i)
theorem
function.update_strict_mono
{ι : Type u_1}
{π : ι → Type u_3}
[decidable_eq ι]
[Π (i : ι), preorder (π i)]
{f : Π (i : ι), π i}
{i : ι} :
strict_mono (function.update f i)