Mathlib.Order.Monotone.Defs

Monotone definition

(f : α → β) : Prop

Full source

/-- A function `f` is monotone if `a ≤ b` implies `f a ≤ f b`. -/
def Monotone (f : α → β) : Prop :=
  ∀ ⦃a b⦄, a ≤ b → f a ≤ f b

Monotone function

Informal description

A function $f : \alpha \to \beta$ between preorders is monotone if for any $a, b \in \alpha$, $a \leq b$ implies $f(a) \leq f(b)$.

Antitone definition

(f : α → β) : Prop

Full source

/-- A function `f` is antitone if `a ≤ b` implies `f b ≤ f a`. -/
def Antitone (f : α → β) : Prop :=
  ∀ ⦃a b⦄, a ≤ b → f b ≤ f a

Antitone function

Informal description

A function $f : \alpha \to \beta$ between preorders is antitone if for any $a, b \in \alpha$, $a \leq b$ implies $f(b) \leq f(a)$.

MonotoneOn definition

(f : α → β) (s : Set α) : Prop

Full source

/-- A function `f` is monotone on `s` if, for all `a, b ∈ s`, `a ≤ b` implies `f a ≤ f b`. -/
def MonotoneOn (f : α → β) (s : Set α) : Prop :=
  ∀ ⦃a⦄ (_ : a ∈ s) ⦃b⦄ (_ : b ∈ s), a ≤ b → f a ≤ f b

Monotone function on a subset

Informal description

A function $f \colon \alpha \to \beta$ between preorders is called *monotone on a subset $s \subseteq \alpha$* if for all $a, b \in s$, the inequality $a \leq b$ implies $f(a) \leq f(b)$.

AntitoneOn definition

(f : α → β) (s : Set α) : Prop

Full source

/-- A function `f` is antitone on `s` if, for all `a, b ∈ s`, `a ≤ b` implies `f b ≤ f a`. -/
def AntitoneOn (f : α → β) (s : Set α) : Prop :=
  ∀ ⦃a⦄ (_ : a ∈ s) ⦃b⦄ (_ : b ∈ s), a ≤ b → f b ≤ f a

Antitone function on a subset

Informal description

A function $f : \alpha \to \beta$ between preorders is antitone on a subset $s \subseteq \alpha$ if for any $a, b \in s$, $a \leq b$ implies $f(b) \leq f(a)$.

StrictMono definition

(f : α → β) : Prop

Full source

/-- A function `f` is strictly monotone if `a < b` implies `f a < f b`. -/
def StrictMono (f : α → β) : Prop :=
  ∀ ⦃a b⦄, a < b → f a < f b

Strictly monotone function

Informal description

A function $f : \alpha \to \beta$ between two preorders is strictly monotone if for any $a, b \in \alpha$, $a < b$ implies $f(a) < f(b)$.

StrictAnti definition

(f : α → β) : Prop

Full source

/-- A function `f` is strictly antitone if `a < b` implies `f b < f a`. -/
def StrictAnti (f : α → β) : Prop :=
  ∀ ⦃a b⦄, a < b → f b < f a

Strictly antitone function

Informal description

A function $f : \alpha \to \beta$ between two preorders is strictly antitone if for any $a, b \in \alpha$, $a < b$ implies $f(b) < f(a)$.

StrictMonoOn definition

(f : α → β) (s : Set α) : Prop

Full source

/-- A function `f` is strictly monotone on `s` if, for all `a, b ∈ s`, `a < b` implies
`f a < f b`. -/
def StrictMonoOn (f : α → β) (s : Set α) : Prop :=
  ∀ ⦃a⦄ (_ : a ∈ s) ⦃b⦄ (_ : b ∈ s), a < b → f a < f b

Strictly monotone function on a subset

Informal description

A function $f : \alpha \to \beta$ between two preorders is strictly monotone on a subset $s \subseteq \alpha$ if for any $a, b \in s$, the inequality $a < b$ implies $f(a) < f(b)$.

StrictAntiOn definition

(f : α → β) (s : Set α) : Prop

Full source

/-- A function `f` is strictly antitone on `s` if, for all `a, b ∈ s`, `a < b` implies
`f b < f a`. -/
def StrictAntiOn (f : α → β) (s : Set α) : Prop :=
  ∀ ⦃a⦄ (_ : a ∈ s) ⦃b⦄ (_ : b ∈ s), a < b → f b < f a

Strictly antitone function on a subset

Informal description

A function $f : \alpha \to \beta$ between two preorders is strictly antitone on a subset $s \subseteq \alpha$ if for all $a, b \in s$, the inequality $a < b$ implies $f(b) < f(a)$.

instDecidableMonotoneOfForallForallForallLe instance

[i : Decidable (∀ a b, a ≤ b → f a ≤ f b)] : Decidable (Monotone f)

Full source

instance [i : Decidable (∀ a b, a ≤ b → f a ≤ f b)] : Decidable (Monotone f) := i

Decidability of Monotone Functions

Informal description

Given a function $f : \alpha \to \beta$ between preorders, if we can decide whether for all $a, b \in \alpha$, $a \leq b$ implies $f(a) \leq f(b)$, then we can decide whether $f$ is monotone.

instDecidableAntitoneOfForallForallForallLe instance

[i : Decidable (∀ a b, a ≤ b → f b ≤ f a)] : Decidable (Antitone f)

Full source

instance [i : Decidable (∀ a b, a ≤ b → f b ≤ f a)] : Decidable (Antitone f) := i

Decidability of Antitone Functions

Informal description

Given a function $f : \alpha \to \beta$ between preorders, if we can decide whether for all $a, b \in \alpha$, $a \leq b$ implies $f(b) \leq f(a)$, then we can decide whether $f$ is antitone.

instDecidableMonotoneOnOfForallForallMemSetForallForallForallLe instance

[i : Decidable (∀ a ∈ s, ∀ b ∈ s, a ≤ b → f a ≤ f b)] : Decidable (MonotoneOn f s)

Full source

instance [i : Decidable (∀ a ∈ s, ∀ b ∈ s, a ≤ b → f a ≤ f b)] :
    Decidable (MonotoneOn f s) := i

Decidability of Monotonicity on a Subset

Informal description

Given a function $f \colon \alpha \to \beta$ between preorders and a subset $s \subseteq \alpha$, if we can decide whether for all $a, b \in s$, $a \leq b$ implies $f(a) \leq f(b)$, then we can decide whether $f$ is monotone on $s$.

instDecidableAntitoneOnOfForallForallMemSetForallForallForallLe instance

[i : Decidable (∀ a ∈ s, ∀ b ∈ s, a ≤ b → f b ≤ f a)] : Decidable (AntitoneOn f s)

Full source

instance [i : Decidable (∀ a ∈ s, ∀ b ∈ s, a ≤ b → f b ≤ f a)] :
    Decidable (AntitoneOn f s) := i

Decidability of Antitone Functions on Subsets

Informal description

Given a function $f \colon \alpha \to \beta$ between preorders and a subset $s \subseteq \alpha$, if there exists a decidable procedure to determine whether for all $a, b \in s$, $a \leq b$ implies $f(b) \leq f(a)$, then the property of $f$ being antitone on $s$ is decidable.

instDecidableStrictMonoOfForallForallForallLt instance

[i : Decidable (∀ a b, a < b → f a < f b)] : Decidable (StrictMono f)

Full source

instance [i : Decidable (∀ a b, a < b → f a < f b)] : Decidable (StrictMono f) := i

Decidability of Strict Monotonicity for Functions Between Preorders

Informal description

For any function $f : \alpha \to \beta$ between preorders, if there is a decidable procedure to determine whether $f$ is strictly monotone (i.e., for all $a, b \in \alpha$, $a < b$ implies $f(a) < f(b)$), then the property `StrictMono f` is decidable.

instDecidableStrictAntiOfForallForallForallLt instance

[i : Decidable (∀ a b, a < b → f b < f a)] : Decidable (StrictAnti f)

Full source

instance [i : Decidable (∀ a b, a < b → f b < f a)] : Decidable (StrictAnti f) := i

Decidability of Strict Antitonicity for Functions Between Preorders

Informal description

For any function $f : \alpha \to \beta$ between preorders, if there is a decidable procedure to determine whether $f$ is strictly antitone (i.e., for all $a, b \in \alpha$, $a < b$ implies $f(b) < f(a)$), then the property `StrictAnti f` is decidable.

instDecidableStrictMonoOnOfForallForallMemSetForallForallForallLt instance

[i : Decidable (∀ a ∈ s, ∀ b ∈ s, a < b → f a < f b)] : Decidable (StrictMonoOn f s)

Full source

instance [i : Decidable (∀ a ∈ s, ∀ b ∈ s, a < b → f a < f b)] :
    Decidable (StrictMonoOn f s) := i

Decidability of Strict Monotonicity on a Subset

Informal description

For any function $f : \alpha \to \beta$ between preorders and any subset $s \subseteq \alpha$, if there is a decidable procedure to determine whether $f$ is strictly monotone on $s$ (i.e., for all $a, b \in s$, $a < b$ implies $f(a) < f(b)$), then the property `StrictMonoOn f s` is decidable.

instDecidableStrictAntiOnOfForallForallMemSetForallForallForallLt instance

[i : Decidable (∀ a ∈ s, ∀ b ∈ s, a < b → f b < f a)] : Decidable (StrictAntiOn f s)

Full source

instance [i : Decidable (∀ a ∈ s, ∀ b ∈ s, a < b → f b < f a)] :
    Decidable (StrictAntiOn f s) := i

Decidability of Strictly Antitone Functions on a Subset

Informal description

For any function $f : \alpha \to \beta$ between preorders and any subset $s \subseteq \alpha$, if there is a decidable procedure to determine whether $f$ is strictly antitone on $s$ (i.e., for all $a, b \in s$, $a < b$ implies $f(b) < f(a)$), then the property `StrictAntiOn f s` is decidable.

Monotone.comp_le_comp_left theorem

 [Preorder β] {f : β → α} {g h : γ → β} (hf : Monotone f) (le_gh : g ≤ h) : LE.le.{max w u} (f ∘ g) (f ∘ h)

Full source

theorem Monotone.comp_le_comp_left
    [Preorder β] {f : β → α} {g h : γ → β} (hf : Monotone f) (le_gh : g ≤ h) :
    LE.le.{max w u} (f ∘ g) (f ∘ h) :=
  fun x ↦ hf (le_gh x)

Monotonicity Preserved Under Composition with Pointwise Order

Informal description

Let $\alpha$, $\beta$, and $\gamma$ be types equipped with preorders. Given a monotone function $f \colon \beta \to \alpha$ and functions $g, h \colon \gamma \to \beta$ such that $g \leq h$ (pointwise), then the composition $f \circ g \leq f \circ h$ (pointwise).

monotone_lam theorem

{f : α → β → γ} (hf : ∀ b, Monotone fun a ↦ f a b) : Monotone f

Full source

theorem monotone_lam {f : α → β → γ} (hf : ∀ b, Monotone fun a ↦ f a b) : Monotone f :=
  fun _ _ h b ↦ hf b h

Monotonicity in the First Argument of a Two-Variable Function

Informal description

Let $f : \alpha \to \beta \to \gamma$ be a function such that for every $b \in \beta$, the function $a \mapsto f(a, b)$ is monotone. Then $f$ is monotone in its first argument, i.e., for any $a_1, a_2 \in \alpha$ with $a_1 \leq a_2$, we have $f(a_1, b) \leq f(a_2, b)$ for all $b \in \beta$.

monotone_app theorem

(f : β → α → γ) (b : β) (hf : Monotone fun a b ↦ f b a) : Monotone (f b)

Full source

theorem monotone_app (f : β → α → γ) (b : β) (hf : Monotone fun a b ↦ f b a) : Monotone (f b) :=
  fun _ _ h ↦ hf h b

Monotonicity Preserved Under Function Application

Informal description

Let $f : \beta \to \alpha \to \gamma$ be a function and fix $b \in \beta$. If the function $\lambda (a, b) \mapsto f(b)(a)$ is monotone (i.e., for any $a_1 \leq a_2$ and any $b$, $f(b)(a_1) \leq f(b)(a_2)$), then the function $f(b) : \alpha \to \gamma$ is monotone. In other words, for any $a_1, a_2 \in \alpha$ with $a_1 \leq a_2$, we have $f(b)(a_1) \leq f(b)(a_2)$.

antitone_lam theorem

{f : α → β → γ} (hf : ∀ b, Antitone fun a ↦ f a b) : Antitone f

Full source

theorem antitone_lam {f : α → β → γ} (hf : ∀ b, Antitone fun a ↦ f a b) : Antitone f :=
  fun _ _ h b ↦ hf b h

Antitonicity in the First Argument of a Two-Variable Function

Informal description

Let $f : \alpha \to \beta \to \gamma$ be a function such that for every $b \in \beta$, the function $a \mapsto f(a, b)$ is antitone. Then $f$ is antitone in its first argument, i.e., for any $a_1, a_2 \in \alpha$ with $a_1 \leq a_2$, we have $f(a_1, b) \geq f(a_2, b)$ for all $b \in \beta$.

antitone_app theorem

(f : β → α → γ) (b : β) (hf : Antitone fun a b ↦ f b a) : Antitone (f b)

Full source

theorem antitone_app (f : β → α → γ) (b : β) (hf : Antitone fun a b ↦ f b a) : Antitone (f b) :=
  fun _ _ h ↦ hf h b

Antitone Property Preserved Under Function Application

Informal description

Let $f : \beta \to \alpha \to \gamma$ be a function and $b \in \beta$. If the function $\lambda a b \mapsto f(b)(a)$ is antitone, then the function $f(b) : \alpha \to \gamma$ is antitone. In other words, if for all $a_1, a_2 \in \alpha$ and $b_1, b_2 \in \beta$, $a_1 \leq a_2$ implies $f(b_2)(a_1) \geq f(b_2)(a_2)$, then for any fixed $b \in \beta$, the function $f(b)$ is antitone in its argument.

Function.monotone_eval theorem

 {ι : Type u} {α : ι → Type v} [∀ i, Preorder (α i)] (i : ι) : Monotone (Function.eval i : (∀ i, α i) → α i)

Full source

theorem Function.monotone_eval {ι : Type u} {α : ι → Type v} [∀ i, Preorder (α i)] (i : ι) :
    Monotone (Function.eval i : (∀ i, α i) → α i) := fun _ _ H ↦ H i

Monotonicity of Pointwise Evaluation in Function Spaces

Informal description

For any family of types $\alpha_i$ indexed by $i \in \iota$, where each $\alpha_i$ is equipped with a preorder, and for any fixed index $i \in \iota$, the evaluation function at $i$ (i.e., the function $\lambda f \mapsto f(i)$ from $(\forall i, \alpha_i)$ to $\alpha_i$) is monotone. In other words, if $f, g \in \forall i, \alpha_i$ satisfy $f \leq g$ (pointwise), then $f(i) \leq g(i)$.

Monotone.imp theorem

(hf : Monotone f) (h : a ≤ b) : f a ≤ f b

Full source

theorem Monotone.imp (hf : Monotone f) (h : a ≤ b) : f a ≤ f b :=
  hf h

Monotonicity Preserves Order

Informal description

For any monotone function $f : \alpha \to \beta$ between preorders and any elements $a, b \in \alpha$, if $a \leq b$, then $f(a) \leq f(b)$.

Antitone.imp theorem

(hf : Antitone f) (h : a ≤ b) : f b ≤ f a

Full source

theorem Antitone.imp (hf : Antitone f) (h : a ≤ b) : f b ≤ f a :=
  hf h

Antitone Function Preserves Order Reversely

Informal description

For any antitone function $f : \alpha \to \beta$ between preorders and any elements $a, b \in \alpha$, if $a \leq b$, then $f(b) \leq f(a)$.

StrictMono.imp theorem

(hf : StrictMono f) (h : a < b) : f a < f b

Full source

theorem StrictMono.imp (hf : StrictMono f) (h : a < b) : f a < f b :=
  hf h

Strictly Monotone Function Preserves Strict Order

Informal description

For any strictly monotone function $f : \alpha \to \beta$ between preorders and any elements $a, b \in \alpha$, if $a < b$, then $f(a) < f(b)$.

StrictAnti.imp theorem

(hf : StrictAnti f) (h : a < b) : f b < f a

Full source

theorem StrictAnti.imp (hf : StrictAnti f) (h : a < b) : f b < f a :=
  hf h

Strictly Antitone Function Preserves Strict Order Reversely

Informal description

For any strictly antitone function $f : \alpha \to \beta$ between preorders and any elements $a, b \in \alpha$, if $a < b$, then $f(b) < f(a)$.

Monotone.monotoneOn theorem

(hf : Monotone f) (s : Set α) : MonotoneOn f s

Full source

protected theorem Monotone.monotoneOn (hf : Monotone f) (s : Set α) : MonotoneOn f s :=
  fun _ _ _ _ ↦ hf.imp

Restriction of Monotone Function to Subset is Monotone

Informal description

If a function $f \colon \alpha \to \beta$ between preorders is monotone, then for any subset $s \subseteq \alpha$, the restriction of $f$ to $s$ is also monotone. That is, for all $a, b \in s$, $a \leq b$ implies $f(a) \leq f(b)$.

Antitone.antitoneOn theorem

(hf : Antitone f) (s : Set α) : AntitoneOn f s

Full source

protected theorem Antitone.antitoneOn (hf : Antitone f) (s : Set α) : AntitoneOn f s :=
  fun _ _ _ _ ↦ hf.imp

Restriction of Antitone Function to Subset is Antitone

Informal description

If a function $f : \alpha \to \beta$ between preorders is antitone (i.e., $a \leq b$ implies $f(b) \leq f(a)$ for all $a, b \in \alpha$), then for any subset $s \subseteq \alpha$, the restriction of $f$ to $s$ is also antitone (i.e., $a \leq b$ implies $f(b) \leq f(a)$ for all $a, b \in s$).

monotoneOn_univ theorem

: MonotoneOn f Set.univ ↔ Monotone f

Full source

@[simp] theorem monotoneOn_univ : MonotoneOnMonotoneOn f Set.univ ↔ Monotone f :=
  ⟨fun h _ _ ↦ h trivial trivial, fun h ↦ h.monotoneOn _⟩

Monotonicity on Universal Set is Equivalent to Global Monotonicity

Informal description

A function $f \colon \alpha \to \beta$ between preorders is monotone on the universal set $\text{univ} = \alpha$ if and only if it is monotone. In other words, $f$ satisfies $a \leq b \implies f(a) \leq f(b)$ for all $a, b \in \alpha$ if and only if it satisfies this condition for all $a, b \in \text{univ}$.

antitoneOn_univ theorem

: AntitoneOn f Set.univ ↔ Antitone f

Full source

@[simp] theorem antitoneOn_univ : AntitoneOnAntitoneOn f Set.univ ↔ Antitone f :=
  ⟨fun h _ _ ↦ h trivial trivial, fun h ↦ h.antitoneOn _⟩

Antitone Function on Universal Set is Antitone

Informal description

A function $f : \alpha \to \beta$ between preorders is antitone on the universal set $\text{univ} \subseteq \alpha$ if and only if it is antitone on the entire type $\alpha$. In other words, $f$ satisfies $a \leq b \implies f(b) \leq f(a)$ for all $a, b \in \text{univ}$ if and only if it satisfies this condition for all $a, b \in \alpha$.

StrictMono.strictMonoOn theorem

(hf : StrictMono f) (s : Set α) : StrictMonoOn f s

Full source

protected theorem StrictMono.strictMonoOn (hf : StrictMono f) (s : Set α) : StrictMonoOn f s :=
  fun _ _ _ _ ↦ hf.imp

Restriction of Strictly Monotone Function is Strictly Monotone

Informal description

If a function $f : \alpha \to \beta$ between two preorders is strictly monotone, then for any subset $s \subseteq \alpha$, the restriction of $f$ to $s$ is also strictly monotone. In other words, if $f$ satisfies $a < b \implies f(a) < f(b)$ for all $a, b \in \alpha$, then for any $a, b \in s$, $a < b$ implies $f(a) < f(b)$.

StrictAnti.strictAntiOn theorem

(hf : StrictAnti f) (s : Set α) : StrictAntiOn f s

Full source

protected theorem StrictAnti.strictAntiOn (hf : StrictAnti f) (s : Set α) : StrictAntiOn f s :=
  fun _ _ _ _ ↦ hf.imp

Restriction of Strictly Antitone Function is Strictly Antitone

Informal description

If a function $f : \alpha \to \beta$ between two preorders is strictly antitone, then for any subset $s \subseteq \alpha$, the restriction of $f$ to $s$ is also strictly antitone. That is, for all $a, b \in s$, if $a < b$, then $f(b) < f(a)$.

strictMonoOn_univ theorem

: StrictMonoOn f Set.univ ↔ StrictMono f

Full source

@[simp] theorem strictMonoOn_univ : StrictMonoOnStrictMonoOn f Set.univ ↔ StrictMono f :=
  ⟨fun h _ _ ↦ h trivial trivial, fun h ↦ h.strictMonoOn _⟩

Strict Monotonicity on Universal Set is Equivalent to Strict Monotonicity

Informal description

A function $f : \alpha \to \beta$ between two preorders is strictly monotone on the universal set (i.e., for all $a, b \in \alpha$) if and only if it is strictly monotone.

strictAntiOn_univ theorem

: StrictAntiOn f Set.univ ↔ StrictAnti f

Full source

@[simp] theorem strictAntiOn_univ : StrictAntiOnStrictAntiOn f Set.univ ↔ StrictAnti f :=
  ⟨fun h _ _ ↦ h trivial trivial, fun h ↦ h.strictAntiOn _⟩

Strictly Antitone on Universal Set iff Strictly Antitone

Informal description

A function $f : \alpha \to \beta$ between two preorders is strictly antitone on the universal set $\text{univ} \subseteq \alpha$ if and only if it is strictly antitone. In other words, $f$ satisfies $f(b) < f(a)$ for all $a, b \in \alpha$ with $a < b$ if and only if it satisfies this condition for all $a, b \in \text{univ}$.

Monotone.strictMono_of_injective theorem

(h₁ : Monotone f) (h₂ : Injective f) : StrictMono f

Full source

theorem Monotone.strictMono_of_injective (h₁ : Monotone f) (h₂ : Injective f) : StrictMono f :=
  fun _ _ h ↦ (h₁ h.le).lt_of_ne fun H ↦ h.ne <| h₂ H

Injective Monotone Functions are Strictly Monotone

Informal description

Let $f : \alpha \to \beta$ be a function between preorders. If $f$ is monotone (i.e., $a \leq b$ implies $f(a) \leq f(b)$) and injective, then $f$ is strictly monotone (i.e., $a < b$ implies $f(a) < f(b)$).

Antitone.strictAnti_of_injective theorem

(h₁ : Antitone f) (h₂ : Injective f) : StrictAnti f

Full source

theorem Antitone.strictAnti_of_injective (h₁ : Antitone f) (h₂ : Injective f) : StrictAnti f :=
  fun _ _ h ↦ (h₁ h.le).lt_of_ne fun H ↦ h.ne <| h₂ H.symm

Injective Antitone Functions are Strictly Antitone

Informal description

Let $f : \alpha \to \beta$ be a function between preorders. If $f$ is antitone (i.e., $a \leq b$ implies $f(b) \leq f(a)$) and injective, then $f$ is strictly antitone (i.e., $a < b$ implies $f(b) < f(a)$).

monotone_iff_forall_lt theorem

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

Full source

theorem monotone_iff_forall_lt : MonotoneMonotone f ↔ ∀ ⦃a b⦄, a < b → f a ≤ f b :=
  forall₂_congr fun _ _ ↦
    ⟨fun hf h ↦ hf h.le, fun hf h ↦ h.eq_or_lt.elim (fun H ↦ (congr_arg _ H).le) hf⟩

Characterization of Monotone Functions via Strict Inequality

Informal description

A function $f : \alpha \to \beta$ between preorders is monotone if and only if for all $a, b \in \alpha$ with $a < b$, we have $f(a) \leq f(b)$.

antitone_iff_forall_lt theorem

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

Full source

theorem antitone_iff_forall_lt : AntitoneAntitone f ↔ ∀ ⦃a b⦄, a < b → f b ≤ f a :=
  forall₂_congr fun _ _ ↦
    ⟨fun hf h ↦ hf h.le, fun hf h ↦ h.eq_or_lt.elim (fun H ↦ (congr_arg _ H).ge) hf⟩

Characterization of Antitone Functions via Strict Inequality

Informal description

A function $f : \alpha \to \beta$ between preorders is antitone if and only if for all $a, b \in \alpha$ with $a < b$, we have $f(b) \leq f(a)$.

monotoneOn_iff_forall_lt theorem

: MonotoneOn f s ↔ ∀ ⦃a⦄ (_ : a ∈ s) ⦃b⦄ (_ : b ∈ s), a < b → f a ≤ f b

Full source

theorem monotoneOn_iff_forall_lt :
    MonotoneOnMonotoneOn f s ↔ ∀ ⦃a⦄ (_ : a ∈ s) ⦃b⦄ (_ : b ∈ s), a < b → f a ≤ f b :=
  ⟨fun hf _ ha _ hb h ↦ hf ha hb h.le,
   fun hf _ ha _ hb h ↦ h.eq_or_lt.elim (fun H ↦ (congr_arg _ H).le) (hf ha hb)⟩

Characterization of Monotone Functions on a Subset via Strict Inequality

Informal description

A function $f \colon \alpha \to \beta$ between preorders is monotone on a subset $s \subseteq \alpha$ if and only if for all $a, b \in s$ with $a < b$, we have $f(a) \leq f(b)$.

antitoneOn_iff_forall_lt theorem

: AntitoneOn f s ↔ ∀ ⦃a⦄ (_ : a ∈ s) ⦃b⦄ (_ : b ∈ s), a < b → f b ≤ f a

Full source

theorem antitoneOn_iff_forall_lt :
    AntitoneOnAntitoneOn f s ↔ ∀ ⦃a⦄ (_ : a ∈ s) ⦃b⦄ (_ : b ∈ s), a < b → f b ≤ f a :=
  ⟨fun hf _ ha _ hb h ↦ hf ha hb h.le,
   fun hf _ ha _ hb h ↦ h.eq_or_lt.elim (fun H ↦ (congr_arg _ H).ge) (hf ha hb)⟩

Characterization of Antitone Functions on a Subset via Strict Inequality

Informal description

A function $f : \alpha \to \beta$ between preorders is antitone on a subset $s \subseteq \alpha$ if and only if for all $a, b \in s$ with $a < b$, we have $f(b) \leq f(a)$.

StrictMonoOn.monotoneOn theorem

(hf : StrictMonoOn f s) : MonotoneOn f s

Full source

protected theorem StrictMonoOn.monotoneOn (hf : StrictMonoOn f s) : MonotoneOn f s :=
  monotoneOn_iff_forall_lt.2 fun _ ha _ hb h ↦ (hf ha hb h).le

Strictly monotone functions on a subset are monotone

Informal description

If a function $f \colon \alpha \to \beta$ between preorders is strictly monotone on a subset $s \subseteq \alpha$ (i.e., for all $a, b \in s$, $a < b$ implies $f(a) < f(b)$), then $f$ is also monotone on $s$ (i.e., for all $a, b \in s$, $a \leq b$ implies $f(a) \leq f(b)$).

StrictAntiOn.antitoneOn theorem

(hf : StrictAntiOn f s) : AntitoneOn f s

Full source

protected theorem StrictAntiOn.antitoneOn (hf : StrictAntiOn f s) : AntitoneOn f s :=
  antitoneOn_iff_forall_lt.2 fun _ ha _ hb h ↦ (hf ha hb h).le

Strictly antitone functions on a subset are antitone

Informal description

If a function $f : \alpha \to \beta$ between preorders is strictly antitone on a subset $s \subseteq \alpha$ (i.e., for all $a, b \in s$, $a < b$ implies $f(b) < f(a)$), then it is also antitone on $s$ (i.e., for all $a, b \in s$, $a \leq b$ implies $f(b) \leq f(a)$).

StrictMono.monotone theorem

(hf : StrictMono f) : Monotone f

Full source

protected theorem StrictMono.monotone (hf : StrictMono f) : Monotone f :=
  monotone_iff_forall_lt.2 fun _ _ h ↦ (hf h).le

Strictly monotone functions are monotone

Informal description

If a function $f : \alpha \to \beta$ between preorders is strictly monotone (i.e., $a < b$ implies $f(a) < f(b)$ for all $a, b \in \alpha$), then it is also monotone (i.e., $a \leq b$ implies $f(a) \leq f(b)$ for all $a, b \in \alpha$).

StrictAnti.antitone theorem

(hf : StrictAnti f) : Antitone f

Full source

protected theorem StrictAnti.antitone (hf : StrictAnti f) : Antitone f :=
  antitone_iff_forall_lt.2 fun _ _ h ↦ (hf h).le

Strictly antitone functions are antitone

Informal description

If a function $f : \alpha \to \beta$ between preorders is strictly antitone (i.e., $a < b$ implies $f(b) < f(a)$ for all $a, b \in \alpha$), then it is also antitone (i.e., $a \leq b$ implies $f(b) \leq f(a)$ for all $a, b \in \alpha$).

Subsingleton.monotone theorem

[Subsingleton α] (f : α → β) : Monotone f

Full source

protected theorem monotone [Subsingleton α] (f : α → β) : Monotone f :=
  fun _ _ _ ↦ (congr_arg _ <| Subsingleton.elim _ _).le

Monotonicity of functions from subsingletons

Informal description

For any function $f : \alpha \to \beta$ where $\alpha$ is a subsingleton (i.e., all elements of $\alpha$ are equal), $f$ is monotone.

Subsingleton.antitone theorem

[Subsingleton α] (f : α → β) : Antitone f

Full source

protected theorem antitone [Subsingleton α] (f : α → β) : Antitone f :=
  fun _ _ _ ↦ (congr_arg _ <| Subsingleton.elim _ _).le

Antitonicity of functions from subsingletons

Informal description

For any function $f : \alpha \to \beta$ where $\alpha$ is a subsingleton (i.e., all elements of $\alpha$ are equal), $f$ is antitone.

Subsingleton.monotone' theorem

[Subsingleton β] (f : α → β) : Monotone f

Full source

theorem monotone' [Subsingleton β] (f : α → β) : Monotone f :=
  fun _ _ _ ↦ (Subsingleton.elim _ _).le

Monotonicity of functions into subsingletons

Informal description

For any function $f : \alpha \to \beta$ where $\beta$ is a subsingleton (i.e., all elements of $\beta$ are equal), $f$ is monotone.

Subsingleton.antitone' theorem

[Subsingleton β] (f : α → β) : Antitone f

Full source

theorem antitone' [Subsingleton β] (f : α → β) : Antitone f :=
  fun _ _ _ ↦ (Subsingleton.elim _ _).le

Antitonicity of Functions into Subsingletons

Informal description

For any function $f : \alpha \to \beta$ where $\beta$ is a subsingleton (i.e., all elements of $\beta$ are equal), $f$ is antitone.

Subsingleton.strictMono theorem

[Subsingleton α] (f : α → β) : StrictMono f

Full source

protected theorem strictMono [Subsingleton α] (f : α → β) : StrictMono f :=
  fun _ _ h ↦ (h.ne <| Subsingleton.elim _ _).elim

Strict Monotonicity of Functions from Subsingletons

Informal description

For any type $\alpha$ with at most one element (i.e., a subsingleton) and any function $f : \alpha \to \beta$ to a preorder $\beta$, the function $f$ is strictly monotone. That is, for any $a, b \in \alpha$, if $a < b$ then $f(a) < f(b)$.

Subsingleton.strictAnti theorem

[Subsingleton α] (f : α → β) : StrictAnti f

Full source

protected theorem strictAnti [Subsingleton α] (f : α → β) : StrictAnti f :=
  fun _ _ h ↦ (h.ne <| Subsingleton.elim _ _).elim

Strictly Antitone Functions from Subsingletons

Informal description

For any type $\alpha$ with at most one element (i.e., a subsingleton) and any function $f : \alpha \to \beta$ to a preorder $\beta$, the function $f$ is strictly antitone. That is, for any $a, b \in \alpha$, if $a < b$ then $f(b) < f(a)$.

monotone_id theorem

[Preorder α] : Monotone (id : α → α)

Full source

theorem monotone_id [Preorder α] : Monotone (id : α → α) := fun _ _ ↦ id

Monotonicity of the Identity Function

Informal description

For any preorder $\alpha$, the identity function $\mathrm{id} : \alpha \to \alpha$ is monotone. That is, for any $a, b \in \alpha$, if $a \leq b$ then $\mathrm{id}(a) \leq \mathrm{id}(b)$.

monotoneOn_id theorem

[Preorder α] {s : Set α} : MonotoneOn id s

Full source

theorem monotoneOn_id [Preorder α] {s : Set α} : MonotoneOn id s := fun _ _ _ _ ↦ id

Monotonicity of Identity Function on a Subset

Informal description

For any preordered type $\alpha$ and any subset $s \subseteq \alpha$, the identity function $\mathrm{id} \colon \alpha \to \alpha$ is monotone on $s$. That is, for all $a, b \in s$, if $a \leq b$ then $\mathrm{id}(a) \leq \mathrm{id}(b)$.

strictMono_id theorem

[Preorder α] : StrictMono (id : α → α)

Full source

theorem strictMono_id [Preorder α] : StrictMono (id : α → α) := fun _ _ ↦ id

Identity Function is Strictly Monotone

Informal description

For any preordered type $\alpha$, the identity function $\mathrm{id} : \alpha \to \alpha$ is strictly monotone. That is, for any $a, b \in \alpha$, if $a < b$ then $\mathrm{id}(a) < \mathrm{id}(b)$.

strictMonoOn_id theorem

[Preorder α] {s : Set α} : StrictMonoOn id s

Full source

theorem strictMonoOn_id [Preorder α] {s : Set α} : StrictMonoOn id s := fun _ _ _ _ ↦ id

Identity Function is Strictly Monotone on a Subset

Informal description

For any preordered type $\alpha$ and any subset $s \subseteq \alpha$, the identity function $\mathrm{id} : \alpha \to \alpha$ is strictly monotone on $s$. That is, for any $a, b \in s$, if $a < b$ then $\mathrm{id}(a) < \mathrm{id}(b)$.

monotone_const theorem

[Preorder α] [Preorder β] {c : β} : Monotone fun _ : α ↦ c

Full source

theorem monotone_const [Preorder α] [Preorder β] {c : β} : Monotone fun _ : α ↦ c :=
  fun _ _ _ ↦ le_rfl

Constant Functions are Monotone

Informal description

For any constant function $f : \alpha \to \beta$ between preorders, where $f(x) = c$ for some fixed $c \in \beta$, the function $f$ is monotone. That is, for any $a, b \in \alpha$, $a \leq b$ implies $f(a) \leq f(b)$ (which simplifies to $c \leq c$).

monotoneOn_const theorem

[Preorder α] [Preorder β] {c : β} {s : Set α} : MonotoneOn (fun _ : α ↦ c) s

Full source

theorem monotoneOn_const [Preorder α] [Preorder β] {c : β} {s : Set α} :
    MonotoneOn (fun _ : α ↦ c) s :=
  fun _ _ _ _ _ ↦ le_rfl

Monotonicity of Constant Functions on Subsets

Informal description

For any preordered types $\alpha$ and $\beta$, a constant function $f \colon \alpha \to \beta$ (where $f(x) = c$ for some fixed $c \in \beta$) is monotone on any subset $s \subseteq \alpha$. That is, for all $a, b \in s$, $a \leq b$ implies $f(a) \leq f(b)$ (which simplifies to $c \leq c$).

antitone_const theorem

[Preorder α] [Preorder β] {c : β} : Antitone fun _ : α ↦ c

Full source

theorem antitone_const [Preorder α] [Preorder β] {c : β} : Antitone fun _ : α ↦ c :=
  fun _ _ _ ↦ le_refl c

Constant Functions are Antitone

Informal description

For any constant function $f : \alpha \to \beta$ between preorders, where $f(x) = c$ for some fixed $c \in \beta$, the function $f$ is antitone. That is, for any $a, b \in \alpha$, $a \leq b$ implies $f(b) \leq f(a)$ (which simplifies to $c \leq c$).

antitoneOn_const theorem

[Preorder α] [Preorder β] {c : β} {s : Set α} : AntitoneOn (fun _ : α ↦ c) s

Full source

theorem antitoneOn_const [Preorder α] [Preorder β] {c : β} {s : Set α} :
    AntitoneOn (fun _ : α ↦ c) s :=
  fun _ _ _ _ _ ↦ le_rfl

Constant Functions are Antitone on Any Subset

Informal description

For any constant function $f : \alpha \to \beta$ between preorders, where $f(x) = c$ for some fixed $c \in \beta$, and for any subset $s \subseteq \alpha$, the function $f$ is antitone on $s$. That is, for any $a, b \in s$, $a \leq b$ implies $f(b) \leq f(a)$ (which simplifies to $c \leq c$).

strictMono_of_le_iff_le theorem

[Preorder α] [Preorder β] {f : α → β} (h : ∀ x y, x ≤ y ↔ f x ≤ f y) : StrictMono f

Full source

theorem strictMono_of_le_iff_le [Preorder α] [Preorder β] {f : α → β}
    (h : ∀ x y, x ≤ y ↔ f x ≤ f y) : StrictMono f :=
  fun _ _ ↦ (lt_iff_lt_of_le_iff_le' (h _ _) (h _ _)).1

Strict Monotonicity from Order-Preserving Equivalence

Informal description

Let $\alpha$ and $\beta$ be preorders, and let $f : \alpha \to \beta$ be a function. If for all $x, y \in \alpha$, the inequality $x \leq y$ holds if and only if $f(x) \leq f(y)$, then $f$ is strictly monotone.

strictAnti_of_le_iff_le theorem

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

Full source

theorem strictAnti_of_le_iff_le [Preorder α] [Preorder β] {f : α → β}
    (h : ∀ x y, x ≤ y ↔ f y ≤ f x) : StrictAnti f :=
  fun _ _ ↦ (lt_iff_lt_of_le_iff_le' (h _ _) (h _ _)).1

Strict Antitonicity from Order-Reversing Equivalence

Informal description

Let $\alpha$ and $\beta$ be preorders, and let $f : \alpha \to \beta$ be a function. If for all $x, y \in \alpha$, the inequality $x \leq y$ holds if and only if $f(y) \leq f(x)$, then $f$ is strictly antitone (i.e., $x < y$ implies $f(y) < f(x)$).

injective_of_lt_imp_ne theorem

[LinearOrder α] {f : α → β} (h : ∀ x y, x < y → f x ≠ f y) : Injective f

Full source

theorem injective_of_lt_imp_ne [LinearOrder α] {f : α → β} (h : ∀ x y, x < y → f x ≠ f y) :
    Injective f := by
  intro x y hf
  rcases lt_trichotomy x y with (hxy | rfl | hxy)
  · exact absurd hf <| h _ _ hxy
  · rfl
  · exact absurd hf.symm <| h _ _ hxy

Injectivity via Strict Inequality Preservation

Informal description

Let $\alpha$ be a linearly ordered set and $\beta$ an arbitrary type. For a function $f : \alpha \to \beta$, if for all $x, y \in \alpha$ the inequality $x < y$ implies $f(x) \neq f(y)$, then $f$ is injective.

injective_of_le_imp_le theorem

[PartialOrder α] [Preorder β] (f : α → β) (h : ∀ {x y}, f x ≤ f y → x ≤ y) : Injective f

Full source

theorem injective_of_le_imp_le [PartialOrder α] [Preorder β] (f : α → β)
    (h : ∀ {x y}, f x ≤ f y → x ≤ y) : Injective f :=
  fun _ _ hxy ↦ (h hxy.le).antisymm (h hxy.ge)

Injectivity via Monotonicity of Preimages

Informal description

Let $\alpha$ be a partially ordered set and $\beta$ a preordered set. Given a function $f : \alpha \to \beta$, if for all $x, y \in \alpha$ the inequality $f(x) \leq f(y)$ implies $x \leq y$, then $f$ is injective.

Monotone.comp theorem

(hg : Monotone g) (hf : Monotone f) : Monotone (g ∘ f)

Full source

protected theorem Monotone.comp (hg : Monotone g) (hf : Monotone f) : Monotone (g ∘ f) :=
  fun _ _ h ↦ hg (hf h)

Composition of Monotone Functions is Monotone

Informal description

Let $\alpha$, $\beta$, and $\gamma$ be preorders. If $f : \alpha \to \beta$ and $g : \beta \to \gamma$ are monotone functions, then their composition $g \circ f : \alpha \to \gamma$ is also monotone. That is, for any $a, b \in \alpha$, if $a \leq b$, then $(g \circ f)(a) \leq (g \circ f)(b)$.

Monotone.comp_antitone theorem

(hg : Monotone g) (hf : Antitone f) : Antitone (g ∘ f)

Full source

theorem Monotone.comp_antitone (hg : Monotone g) (hf : Antitone f) : Antitone (g ∘ f) :=
  fun _ _ h ↦ hg (hf h)

Composition of Monotone and Antitone Functions is Antitone

Informal description

Let $f : \alpha \to \beta$ be an antitone function and $g : \beta \to \gamma$ be a monotone function between preorders. Then the composition $g \circ f : \alpha \to \gamma$ is antitone.

Antitone.comp theorem

(hg : Antitone g) (hf : Antitone f) : Monotone (g ∘ f)

Full source

protected theorem Antitone.comp (hg : Antitone g) (hf : Antitone f) : Monotone (g ∘ f) :=
  fun _ _ h ↦ hg (hf h)

Composition of Antitone Functions is Monotone

Informal description

Let $f : \alpha \to \beta$ and $g : \beta \to \gamma$ be antitone functions between preorders. Then the composition $g \circ f : \alpha \to \gamma$ is monotone.

Antitone.comp_monotone theorem

(hg : Antitone g) (hf : Monotone f) : Antitone (g ∘ f)

Full source

theorem Antitone.comp_monotone (hg : Antitone g) (hf : Monotone f) : Antitone (g ∘ f) :=
  fun _ _ h ↦ hg (hf h)

Composition of Monotone and Antitone Functions is Antitone

Informal description

Let $f : \alpha \to \beta$ be a monotone function and $g : \beta \to \gamma$ be an antitone function between preorders. Then the composition $g \circ f : \alpha \to \gamma$ is antitone.

Monotone.iterate theorem

{f : α → α} (hf : Monotone f) (n : ℕ) : Monotone f^[n]

Full source

protected theorem Monotone.iterate {f : α → α} (hf : Monotone f) (n : ℕ) : Monotone f^[n] :=
  Nat.recOn n monotone_id fun _ h ↦ h.comp hf

Monotonicity of Iterated Function $f^{[n]}$

Informal description

Let $f : \alpha \to \alpha$ be a monotone function on a preorder $\alpha$. Then for any natural number $n$, the $n$-th iterate $f^{[n]}$ of $f$ is also monotone. That is, for any $a, b \in \alpha$, if $a \leq b$ then $f^{[n]}(a) \leq f^{[n]}(b)$.

Monotone.comp_monotoneOn theorem

(hg : Monotone g) (hf : MonotoneOn f s) : MonotoneOn (g ∘ f) s

Full source

protected theorem Monotone.comp_monotoneOn (hg : Monotone g) (hf : MonotoneOn f s) :
    MonotoneOn (g ∘ f) s :=
  fun _ ha _ hb h ↦ hg (hf ha hb h)

Monotonicity of Composition of Monotone Functions on a Subset

Informal description

Let $f \colon \alpha \to \beta$ be a function that is monotone on a subset $s \subseteq \alpha$, and let $g \colon \beta \to \gamma$ be a monotone function. Then the composition $g \circ f$ is monotone on $s$. That is, for any $a, b \in s$, if $a \leq b$ then $(g \circ f)(a) \leq (g \circ f)(b)$.

Monotone.comp_antitoneOn theorem

(hg : Monotone g) (hf : AntitoneOn f s) : AntitoneOn (g ∘ f) s

Full source

theorem Monotone.comp_antitoneOn (hg : Monotone g) (hf : AntitoneOn f s) : AntitoneOn (g ∘ f) s :=
  fun _ ha _ hb h ↦ hg (hf ha hb h)

Composition of Monotone and Antitone Functions is Antitone

Informal description

Let $f : \alpha \to \beta$ be an antitone function on a subset $s \subseteq \alpha$, and let $g : \beta \to \gamma$ be a monotone function. Then the composition $g \circ f$ is antitone on $s$.

Antitone.comp_antitoneOn theorem

(hg : Antitone g) (hf : AntitoneOn f s) : MonotoneOn (g ∘ f) s

Full source

protected theorem Antitone.comp_antitoneOn (hg : Antitone g) (hf : AntitoneOn f s) :
    MonotoneOn (g ∘ f) s :=
  fun _ ha _ hb h ↦ hg (hf ha hb h)

Composition of Antitone Functions is Monotone on a Subset

Informal description

Let $f \colon \alpha \to \beta$ be an antitone function on a subset $s \subseteq \alpha$, and let $g \colon \beta \to \gamma$ be an antitone function. Then the composition $g \circ f$ is monotone on $s$. That is, for any $a, b \in s$, if $a \leq b$ then $(g \circ f)(a) \leq (g \circ f)(b)$.

Antitone.comp_monotoneOn theorem

(hg : Antitone g) (hf : MonotoneOn f s) : AntitoneOn (g ∘ f) s

Full source

theorem Antitone.comp_monotoneOn (hg : Antitone g) (hf : MonotoneOn f s) : AntitoneOn (g ∘ f) s :=
  fun _ ha _ hb h ↦ hg (hf ha hb h)

Composition of Antitone and Monotone Functions is Antitone on a Subset

Informal description

Let $f \colon \alpha \to \beta$ be a monotone function on a subset $s \subseteq \alpha$, and let $g \colon \beta \to \gamma$ be an antitone function. Then the composition $g \circ f$ is antitone on $s$. That is, for any $a, b \in s$, if $a \leq b$ then $(g \circ f)(b) \leq (g \circ f)(a)$.

StrictMono.comp theorem

(hg : StrictMono g) (hf : StrictMono f) : StrictMono (g ∘ f)

Full source

protected theorem StrictMono.comp (hg : StrictMono g) (hf : StrictMono f) : StrictMono (g ∘ f) :=
  fun _ _ h ↦ hg (hf h)

Composition of Strictly Monotone Functions is Strictly Monotone

Informal description

Let $f : \alpha \to \beta$ and $g : \beta \to \gamma$ be strictly monotone functions between preorders. Then the composition $g \circ f : \alpha \to \gamma$ is also strictly monotone. That is, for any $a, b \in \alpha$, if $a < b$ then $g(f(a)) < g(f(b))$.

StrictMono.comp_strictAnti theorem

(hg : StrictMono g) (hf : StrictAnti f) : StrictAnti (g ∘ f)

Full source

theorem StrictMono.comp_strictAnti (hg : StrictMono g) (hf : StrictAnti f) : StrictAnti (g ∘ f) :=
  fun _ _ h ↦ hg (hf h)

Composition of Strictly Monotone and Strictly Antitone Functions is Strictly Antitone

Informal description

Let $f : \alpha \to \beta$ be a strictly antitone function and $g : \beta \to \gamma$ be a strictly monotone function between preorders. Then the composition $g \circ f : \alpha \to \gamma$ is strictly antitone. That is, for any $a, b \in \alpha$, if $a < b$ then $g(f(b)) < g(f(a))$.

StrictAnti.comp theorem

(hg : StrictAnti g) (hf : StrictAnti f) : StrictMono (g ∘ f)

Full source

protected theorem StrictAnti.comp (hg : StrictAnti g) (hf : StrictAnti f) : StrictMono (g ∘ f) :=
  fun _ _ h ↦ hg (hf h)

Composition of Strictly Antitone Functions is Strictly Monotone

Informal description

Let $f : \alpha \to \beta$ and $g : \beta \to \gamma$ be strictly antitone functions between preorders. Then the composition $g \circ f : \alpha \to \gamma$ is strictly monotone. That is, for any $a, b \in \alpha$, if $a < b$ then $g(f(a)) < g(f(b))$.

StrictAnti.comp_strictMono theorem

(hg : StrictAnti g) (hf : StrictMono f) : StrictAnti (g ∘ f)

Full source

theorem StrictAnti.comp_strictMono (hg : StrictAnti g) (hf : StrictMono f) : StrictAnti (g ∘ f) :=
  fun _ _ h ↦ hg (hf h)

Composition of Strictly Antitone and Strictly Monotone Functions is Strictly Antitone

Informal description

Let $f : \alpha \to \beta$ be a strictly monotone function and $g : \beta \to \gamma$ be a strictly antitone function between preorders. Then the composition $g \circ f : \alpha \to \gamma$ is strictly antitone. That is, for any $a, b \in \alpha$, if $a < b$ then $g(f(b)) < g(f(a))$.

StrictMono.iterate theorem

{f : α → α} (hf : StrictMono f) (n : ℕ) : StrictMono f^[n]

Full source

protected theorem StrictMono.iterate {f : α → α} (hf : StrictMono f) (n : ℕ) : StrictMono f^[n] :=
  Nat.recOn n strictMono_id fun _ h ↦ h.comp hf

Iterates of a Strictly Monotone Function are Strictly Monotone

Informal description

Let $f : \alpha \to \alpha$ be a strictly monotone function on a preordered type $\alpha$. Then for any natural number $n$, the $n$-th iterate $f^{[n]}$ of $f$ is also strictly monotone. That is, for any $a, b \in \alpha$, if $a < b$ then $f^{[n]}(a) < f^{[n]}(b)$.

StrictMono.comp_strictMonoOn theorem

(hg : StrictMono g) (hf : StrictMonoOn f s) : StrictMonoOn (g ∘ f) s

Full source

protected theorem StrictMono.comp_strictMonoOn (hg : StrictMono g) (hf : StrictMonoOn f s) :
    StrictMonoOn (g ∘ f) s :=
  fun _ ha _ hb h ↦ hg (hf ha hb h)

Composition of Strictly Monotone Functions Preserves Strict Monotonicity on a Subset

Informal description

Let $f : \alpha \to \beta$ be a function that is strictly monotone on a subset $s \subseteq \alpha$, and let $g : \beta \to \gamma$ be a strictly monotone function. Then the composition $g \circ f$ is strictly monotone on $s$. That is, for any $a, b \in s$, if $a < b$ then $g(f(a)) < g(f(b))$.

StrictMono.comp_strictAntiOn theorem

(hg : StrictMono g) (hf : StrictAntiOn f s) : StrictAntiOn (g ∘ f) s

Full source

theorem StrictMono.comp_strictAntiOn (hg : StrictMono g) (hf : StrictAntiOn f s) :
    StrictAntiOn (g ∘ f) s :=
  fun _ ha _ hb h ↦ hg (hf ha hb h)

Composition of Strictly Monotone and Strictly Antitone Functions Yields Strictly Antitone Function on Subset

Informal description

Let $f : \alpha \to \beta$ be a function that is strictly antitone on a subset $s \subseteq \alpha$, and let $g : \beta \to \gamma$ be a strictly monotone function. Then the composition $g \circ f$ is strictly antitone on $s$. That is, for any $a, b \in s$, if $a < b$ then $g(f(b)) < g(f(a))$.

StrictAnti.comp_strictAntiOn theorem

(hg : StrictAnti g) (hf : StrictAntiOn f s) : StrictMonoOn (g ∘ f) s

Full source

protected theorem StrictAnti.comp_strictAntiOn (hg : StrictAnti g) (hf : StrictAntiOn f s) :
    StrictMonoOn (g ∘ f) s :=
  fun _ ha _ hb h ↦ hg (hf ha hb h)

Composition of Strictly Antitone Functions Yields Strictly Monotone Function on Subset

Informal description

Let $f : \alpha \to \beta$ be a function that is strictly antitone on a subset $s \subseteq \alpha$, and let $g : \beta \to \gamma$ be a strictly antitone function. Then the composition $g \circ f$ is strictly monotone on $s$. That is, for any $a, b \in s$, if $a < b$ then $g(f(a)) < g(f(b))$.

StrictAnti.comp_strictMonoOn theorem

(hg : StrictAnti g) (hf : StrictMonoOn f s) : StrictAntiOn (g ∘ f) s

Full source

theorem StrictAnti.comp_strictMonoOn (hg : StrictAnti g) (hf : StrictMonoOn f s) :
    StrictAntiOn (g ∘ f) s :=
  fun _ ha _ hb h ↦ hg (hf ha hb h)

Composition of Strictly Antitone and Strictly Monotone Functions Yields Strictly Antitone Function on Subset

Informal description

Let $f : \alpha \to \beta$ be a function that is strictly monotone on a subset $s \subseteq \alpha$, and let $g : \beta \to \gamma$ be a strictly antitone function. Then the composition $g \circ f$ is strictly antitone on $s$. That is, for any $a, b \in s$, if $a < b$ then $g(f(b)) < g(f(a))$.

Monotone.reflect_lt theorem

(hf : Monotone f) {a b : α} (h : f a < f b) : a < b

Full source

theorem Monotone.reflect_lt (hf : Monotone f) {a b : α} (h : f a < f b) : a < b :=
  lt_of_not_ge fun h' ↦ h.not_le (hf h')

Monotone Functions Reflect Strict Inequality

Informal description

Let $f : \alpha \to \beta$ be a monotone function between preorders. For any $a, b \in \alpha$, if $f(a) < f(b)$, then $a < b$.

Antitone.reflect_lt theorem

(hf : Antitone f) {a b : α} (h : f a < f b) : b < a

Full source

theorem Antitone.reflect_lt (hf : Antitone f) {a b : α} (h : f a < f b) : b < a :=
  lt_of_not_ge fun h' ↦ h.not_le (hf h')

Antitone Functions Reflect Strict Inequalities: $f(a) < f(b) \Rightarrow b < a$

Informal description

For any antitone function $f : \alpha \to \beta$ between preorders, if $f(a) < f(b)$ for some $a, b \in \alpha$, then $b < a$.

MonotoneOn.reflect_lt theorem

(hf : MonotoneOn f s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) (h : f a < f b) : a < b

Full source

theorem MonotoneOn.reflect_lt (hf : MonotoneOn f s) {a b : α} (ha : a ∈ s) (hb : b ∈ s)
    (h : f a < f b) : a < b :=
  lt_of_not_ge fun h' ↦ h.not_le <| hf hb ha h'

Reflection of Strict Inequality by Monotone Functions on Subsets

Informal description

Let $f \colon \alpha \to \beta$ be a function between preorders, and let $s \subseteq \alpha$. If $f$ is monotone on $s$ (i.e., for all $a, b \in s$, $a \leq b$ implies $f(a) \leq f(b)$), then for any $a, b \in s$ with $f(a) < f(b)$, we have $a < b$.

AntitoneOn.reflect_lt theorem

(hf : AntitoneOn f s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) (h : f a < f b) : b < a

Full source

theorem AntitoneOn.reflect_lt (hf : AntitoneOn f s) {a b : α} (ha : a ∈ s) (hb : b ∈ s)
    (h : f a < f b) : b < a :=
  lt_of_not_ge fun h' ↦ h.not_le <| hf ha hb h'

Antitone Functions Reflect Strict Inequalities on Subsets

Informal description

Let $f : \alpha \to \beta$ be a function between preorders, and let $s \subseteq \alpha$. If $f$ is antitone on $s$ (i.e., for all $a, b \in s$, $a \leq b$ implies $f(b) \leq f(a)$), then for any $a, b \in s$ with $f(a) < f(b)$, we have $b < a$.

Subtype.mono_coe theorem

[Preorder α] (t : Set α) : Monotone ((↑) : Subtype t → α)

Full source

theorem Subtype.mono_coe [Preorder α] (t : Set α) : Monotone ((↑) : Subtype t → α) :=
  fun _ _ ↦ id

Monotonicity of Subtype Inclusion

Informal description

For any preorder on a type $\alpha$ and a subset $t \subseteq \alpha$, the canonical inclusion map $\iota : t \to \alpha$ (which sends an element of the subtype to its underlying element in $\alpha$) is monotone. That is, for any $x, y \in t$, if $x \leq y$ in the induced preorder on $t$, then $\iota(x) \leq \iota(y)$ in $\alpha$.

Subtype.strictMono_coe theorem

[Preorder α] (t : Set α) : StrictMono ((↑) : Subtype t → α)

Full source

theorem Subtype.strictMono_coe [Preorder α] (t : Set α) :
    StrictMono ((↑) : Subtype t → α) :=
  fun _ _ ↦ id

Strict Monotonicity of Subtype Inclusion

Informal description

For any preorder on a type $\alpha$ and a subset $t \subseteq \alpha$, the canonical inclusion map $\iota : t \to \alpha$ (which sends an element of the subtype to its underlying element in $\alpha$) is strictly monotone. That is, for any $x, y \in t$, if $x < y$ in the induced preorder on $t$, then $\iota(x) < \iota(y)$ in $\alpha$.

monotone_fst theorem

: Monotone (@Prod.fst α β)

Full source

theorem monotone_fst : Monotone (@Prod.fst α β) := fun _ _ ↦ And.left

Monotonicity of First Projection

Informal description

The first projection function $\mathrm{fst} : \alpha \times \beta \to \alpha$ is monotone with respect to the product preorder on $\alpha \times \beta$ and the preorder on $\alpha$. That is, for any pairs $(x_1, y_1), (x_2, y_2) \in \alpha \times \beta$, if $(x_1, y_1) \leq (x_2, y_2)$ in the product preorder, then $x_1 \leq x_2$ in $\alpha$.

monotone_snd theorem

: Monotone (@Prod.snd α β)

Full source

theorem monotone_snd : Monotone (@Prod.snd α β) := fun _ _ ↦ And.right

Monotonicity of Second Projection

Informal description

The second projection function $\mathrm{snd} : \alpha \times \beta \to \beta$ is monotone with respect to the product preorder on $\alpha \times \beta$ and the preorder on $\beta$. That is, for any pairs $(x_1, y_1), (x_2, y_2) \in \alpha \times \beta$, if $(x_1, y_1) \leq (x_2, y_2)$ in the product preorder, then $y_1 \leq y_2$ in $\beta$.

Monotone.prodMap theorem

(hf : Monotone f) (hg : Monotone g) : Monotone (Prod.map f g)

Full source

theorem Monotone.prodMap (hf : Monotone f) (hg : Monotone g) : Monotone (Prod.map f g) :=
  fun _ _ h ↦ ⟨hf h.1, hg h.2⟩

Monotonicity of Product Map

Informal description

Let $f : \alpha \to \gamma$ and $g : \beta \to \delta$ be monotone functions between preorders. Then the product map $f \times g : \alpha \times \beta \to \gamma \times \delta$ defined by $(f \times g)(x, y) = (f(x), g(y))$ is also monotone.

Antitone.prodMap theorem

(hf : Antitone f) (hg : Antitone g) : Antitone (Prod.map f g)

Full source

theorem Antitone.prodMap (hf : Antitone f) (hg : Antitone g) : Antitone (Prod.map f g) :=
  fun _ _ h ↦ ⟨hf h.1, hg h.2⟩

Antitonicity of Product Map

Informal description

Let $f : \alpha \to \gamma$ and $g : \beta \to \delta$ be antitone functions between preorders. Then the product map $f \times g : \alpha \times \beta \to \gamma \times \delta$ defined by $(f \times g)(x, y) = (f(x), g(y))$ is also antitone.

monotone_prod_iff theorem

{h : α × β → γ} : Monotone h ↔ (∀ a, Monotone (fun b => h (a, b))) ∧ (∀ b, Monotone (fun a => h (a, b)))

Full source

lemma monotone_prod_iff {h : α × β → γ} :
    MonotoneMonotone h ↔ (∀ a, Monotone (fun b => h (a, b))) ∧ (∀ b, Monotone (fun a => h (a, b))) where
  mp h := ⟨fun _ _ _ hab => h (Prod.mk_le_mk_iff_right.mpr hab),
    fun _ _ _ hab => h (Prod.mk_le_mk_iff_left.mpr hab)⟩
  mpr h _ _ hab := le_trans (h.1 _ (Prod.mk_le_mk.mp hab).2) (h.2 _ (Prod.mk_le_mk.mp hab).1)

Characterization of Monotonicity for Functions on Product Spaces

Informal description

A function $h : \alpha \times \beta \to \gamma$ between preorders is monotone if and only if for every fixed $a \in \alpha$, the function $b \mapsto h(a, b)$ is monotone, and for every fixed $b \in \beta$, the function $a \mapsto h(a, b)$ is monotone.

antitone_prod_iff theorem

{h : α × β → γ} : Antitone h ↔ (∀ a, Antitone (fun b => h (a, b))) ∧ (∀ b, Antitone (fun a => h (a, b)))

Full source

lemma antitone_prod_iff {h : α × β → γ} :
    AntitoneAntitone h ↔ (∀ a, Antitone (fun b => h (a, b))) ∧ (∀ b, Antitone (fun a => h (a, b))) where
  mp h := ⟨fun _ _ _ hab => h (Prod.mk_le_mk_iff_right.mpr hab),
    fun _ _ _ hab => h (Prod.mk_le_mk_iff_left.mpr hab)⟩
  mpr h _ _ hab := le_trans (h.1 _ (Prod.mk_le_mk.mp hab).2) (h.2 _ (Prod.mk_le_mk.mp hab).1)

Characterization of Antitonicity for Functions on Product Spaces

Informal description

A function $h : \alpha \times \beta \to \gamma$ between preorders is antitone if and only if for every fixed $a \in \alpha$, the function $b \mapsto h(a, b)$ is antitone, and for every fixed $b \in \beta$, the function $a \mapsto h(a, b)$ is antitone.

StrictMono.prodMap theorem

(hf : StrictMono f) (hg : StrictMono g) : StrictMono (Prod.map f g)

Full source

theorem StrictMono.prodMap (hf : StrictMono f) (hg : StrictMono g) : StrictMono (Prod.map f g) :=
  fun a b ↦ by
  simp only [Prod.lt_iff]
  exact Or.imp (And.imp hf.imp hg.monotone.imp) (And.imp hf.monotone.imp hg.imp)

Strict Monotonicity of Product Map $f \times g$

Informal description

Let $f : \alpha \to \gamma$ and $g : \beta \to \delta$ be strictly monotone functions between preorders. Then the product map $f \times g : \alpha \times \beta \to \gamma \times \delta$ defined by $(x, y) \mapsto (f(x), g(y))$ is also strictly monotone.

StrictAnti.prodMap theorem

(hf : StrictAnti f) (hg : StrictAnti g) : StrictAnti (Prod.map f g)

Full source

theorem StrictAnti.prodMap (hf : StrictAnti f) (hg : StrictAnti g) : StrictAnti (Prod.map f g) :=
  fun a b ↦ by
  simp only [Prod.lt_iff]
  exact Or.imp (And.imp hf.imp hg.antitone.imp) (And.imp hf.antitone.imp hg.imp)

Strictly Antitone Product Map

Informal description

For any strictly antitone functions $f : \alpha \to \gamma$ and $g : \beta \to \delta$ between preorders, the product map $(f \times g) : \alpha \times \beta \to \gamma \times \delta$ defined by $(x,y) \mapsto (f(x), g(y))$ is also strictly antitone.

Function.update_mono theorem

: Monotone (update f i)

Full source

theorem update_mono : Monotone (update f i) := fun _ _ => update_le_update_iff'.2

Monotonicity of Function Update at a Fixed Index

Informal description

For any function $f$ and index $i$, the function update operation $\text{update } f \, i$ is monotone. That is, for any values $a$ and $b$, if $a \leq b$, then $\text{update } f \, i \, a \leq \text{update } f \, i \, b$.

Function.update_strictMono theorem

: StrictMono (update f i)

Full source

theorem update_strictMono : StrictMono (update f i) := fun _ _ => update_lt_update_iff.2

Strict Monotonicity of Function Update at a Fixed Index

Informal description

For any function $f$ and index $i$, the function update operation $\text{update } f \, i$ is strictly monotone. That is, for any values $a$ and $b$, if $a < b$, then $\text{update } f \, i \, a < \text{update } f \, i \, b$.

Function.const_mono theorem

: Monotone (const β : α → β → α)

Full source

theorem const_mono : Monotone (const β : α → β → α) := fun _ _ h _ ↦ h

Monotonicity of Constant Functions

Informal description

The constant function $\text{const}_\beta : \alpha \to \beta \to \alpha$ is monotone. That is, for any $a, b \in \alpha$, if $a \leq b$, then $\text{const}_\beta a \leq \text{const}_\beta b$.

Function.const_strictMono theorem

[Nonempty β] : StrictMono (const β : α → β → α)

Full source

theorem const_strictMono [Nonempty β] : StrictMono (const β : α → β → α) :=
  fun _ _ ↦ const_lt_const.2

Strict Monotonicity of Constant Functions in Nonempty Preorders

Informal description

For any nonempty type $\beta$ equipped with a preorder, the constant function $\text{const}_\beta : \alpha \to \beta \to \alpha$ is strictly monotone. That is, for any $a, b \in \alpha$, if $a < b$, then $\text{const}_\beta a < \text{const}_\beta b$.

monotone_iff_apply₂ theorem

: Monotone f ↔ ∀ i, Monotone (f · i)

Full source

lemma monotone_iff_apply₂ : MonotoneMonotone f ↔ ∀ i, Monotone (f · i) := by
  simp [Monotone, Pi.le_def, @forall_swap ι]

Monotonicity in Function Spaces is Componentwise Monotonicity

Informal description

A function $f : \alpha \to (\forall i, \pi_i)$ between preorders is monotone if and only if for every index $i$, the component function $f(\cdot)(i) : \alpha \to \pi_i$ is monotone. In other words, $f$ is monotone if and only if for all $i$, $a \leq b$ implies $f(a)(i) \leq f(b)(i)$.

antitone_iff_apply₂ theorem

: Antitone f ↔ ∀ i, Antitone (f · i)

Full source

lemma antitone_iff_apply₂ : AntitoneAntitone f ↔ ∀ i, Antitone (f · i) := by
  simp [Antitone, Pi.le_def, @forall_swap ι]

Antitone Functions in Product Spaces are Componentwise Antitone

Informal description

A function $f : \alpha \to (\forall i, \pi_i)$ between preorders is antitone if and only if for every index $i$, the component function $f(\cdot)(i) : \alpha \to \pi_i$ is antitone. In other words, $f$ is antitone if and only if for all $i$, $a \leq b$ implies $f(b)(i) \leq f(a)(i)$.

Mathlib.Order.Monotone.Defs

Definitions

Implementation notes

Tags