Documentation

Mathlib.Order.Monotone.Defs

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.

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.

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

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 (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

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

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

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

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 monotone_prod_iff {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {h : α × β → γ} :

Monotone h ↔ (∀ (a : α), Monotone fun (b : β) => h (a, b)) ∧ ∀ (b : β), Monotone fun (a : α) => h (a, b)

theorem antitone_prod_iff {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {h : α × β → γ} :

Antitone h ↔ (∀ (a : α), Antitone fun (b : β) => h (a, b)) ∧ ∀ (b : β), Antitone fun (a : α) => h (a, b)

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 (update f i)

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

StrictMono (update f i)

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

Monotone (const β)

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

StrictMono (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.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 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 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₂.