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

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

def MonotoneOn {α : 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

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

def AntitoneOn {α : 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

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

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

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

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

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

def StrictMonoOn {α : 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

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

def StrictAntiOn {α : 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

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

def IsStable {α : Type u_4} {γ : Type u_5} [Preorder α] (f : α → γ) (σ : α → α) : Prop

σ is stable for f if it breaks ties by increasing index: among elements with equal f-value, σ preserves their order. This property does not use the order on the codomain of f, only its equality, so it is unchanged by reversing that order.

Equations

• IsStable f σ = ∀ ⦃i j : α⦄, i ≤ j → f (σ i) = f (σ j) → σ i ≤ σ j

@[instance_reducible]

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_reducible]

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_reducible]

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_reducible]

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_reducible]

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_reducible]

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_reducible]

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_reducible]

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

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

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

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

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 α) : MonotoneOn f s

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

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

theorem Antitone.strictAnti_of_injective {α : Type u} {β : Type v} [Preorder α] [PartialOrder β] {f : α → β} (h₁ : Antitone f) (h₂ : Function.Injective f) : StrictAnti 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) : MonotoneOn f s

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

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

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

Monotonicity from and to subsingletons

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

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

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

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

Miscellaneous monotonicity results

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

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

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

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

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

theorem Function.Injective.of_lt_imp_ne {α : Type u} {β : Type v} [LinearOrder α] {f : α → β} (h : ∀ (x y : α), x < y → f x ≠ f y) : Injective f

theorem Function.Injective.of_eq_imp_le {α : Type u} {β : Type v} [PartialOrder α] {f : α → β} (h : ∀ {x y : α}, f x = f y → x ≤ y) : 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 : ℕ) : 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 MonotoneOn.comp {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {g : β → γ} {f : α → β} {s : Set α} {t : Set β} (hg : MonotoneOn g t) (hf : MonotoneOn f s) (hs : Set.MapsTo f s t) : MonotoneOn (g ∘ f) s

theorem MonotoneOn.comp_AntitoneOn {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {g : β → γ} {f : α → β} {s : Set α} {t : Set β} (hg : MonotoneOn g t) (hf : AntitoneOn f s) (hs : Set.MapsTo f s t) : AntitoneOn (g ∘ f) s

theorem AntitoneOn.comp {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {g : β → γ} {f : α → β} {s : Set α} {t : Set β} (hg : AntitoneOn g t) (hf : AntitoneOn f s) (hs : Set.MapsTo f s t) : MonotoneOn (g ∘ f) s

theorem AntitoneOn.comp_MonotoneOn {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {g : β → γ} {f : α → β} {s : Set α} {t : Set β} (hg : AntitoneOn g t) (hf : MonotoneOn f s) (hs : Set.MapsTo f s t) : AntitoneOn (g ∘ f) s

theorem StrictMonoOn.comp {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {g : β → γ} {f : α → β} {s : Set α} {t : Set β} (hg : StrictMonoOn g t) (hf : StrictMonoOn f s) (hs : Set.MapsTo f s t) : StrictMonoOn (g ∘ f) s

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

theorem StrictAntiOn.comp {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {g : β → γ} {f : α → β} {s : Set α} {t : Set β} (hg : StrictAntiOn g t) (hf : StrictAntiOn f s) (hs : Set.MapsTo f s t) : StrictMonoOn (g ∘ f) s

theorem StrictAntiOn.comp_strictMonoOn {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {g : β → γ} {f : α → β} {s : Set α} {t : Set β} (hg : StrictAntiOn g t) (hf : StrictMonoOn f s) (hs : Set.MapsTo f s t) : 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 α] (p : α → Prop) : Monotone val

theorem Set.mono_coe {α : Type u} [Preorder α] (A : Set α) : Monotone fun (a : ↑A) => ↑a

theorem Subtype.strictMono_coe {α : Type u} [Preorder α] (p : α → Prop) : StrictMono val

theorem Set.strictMono_coe {α : Type u} [Preorder α] (A : Set α) : StrictMono fun (a : ↑A) => ↑a

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_prodMk_iff {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : γ → α} {g : γ → β} : (Monotone fun (x : γ) => (f x, g x)) ↔ Monotone f ∧ Monotone g

theorem Monotone.prodMk {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : γ → α} {g : γ → β} (hf : Monotone f) (hg : Monotone g) : Monotone fun (x : γ) => (f x, g x)

theorem Monotone.prodMap {α : 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.prodMap {α : 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.prodMap {α : 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.prodMap {α : 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.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 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₂.