Mathlib.Order.Monotone.Basic

instDecidableMonotoneOfForallForallForallLe_1 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 Monotonicity from Pointwise Comparison

Informal description

For any function $f : \alpha \to \beta$ between preorders, if there is a decision procedure for the condition $\forall a\, b, a \leq b \to f(a) \leq f(b)$, then there is a decision procedure for whether $f$ is monotone.

instDecidableAntitoneOfForallForallForallLe_1 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 Antitonicity from Pointwise Comparison

Informal description

For any function $f : \alpha \to \beta$ between preorders, if there is a decision procedure for the condition $\forall a\, b, a \leq b \to f(b) \leq f(a)$, then there is a decision procedure for whether $f$ is antitone.

instDecidableMonotoneOnOfForallForallMemSetForallForallForallLe_1 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

For any function $f \colon \alpha \to \beta$ between preorders and any subset $s \subseteq \alpha$, if there is a decision procedure for the condition that for all $a, b \in s$, $a \leq b$ implies $f(a) \leq f(b)$, then the property of $f$ being monotone on $s$ is decidable.

instDecidableAntitoneOnOfForallForallMemSetForallForallForallLe_1 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 Antitonicity on a Subset

Informal description

For any function $f \colon \alpha \to \beta$ between preorders and any subset $s \subseteq \alpha$, if there is a decision procedure for the condition that 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_1 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 Strictly Monotone Functions

Informal description

For any function $f : \alpha \to \beta$ between two 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_1 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 Strictly Antitone Functions

Informal description

For any function $f : \alpha \to \beta$ between two 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_1 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 Strictly Monotone Functions on a Subset

Informal description

For any function $f : \alpha \to \beta$ between two 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 of $f$ being strictly monotone on $s$ is decidable.

instDecidableStrictAntiOnOfForallForallMemSetForallForallForallLt_1 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 two 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_ofDual_iff theorem

: Monotone (f ∘ ofDual) ↔ Antitone f

Full source

@[simp]
theorem monotone_comp_ofDual_iff : MonotoneMonotone (f ∘ ofDual) ↔ Antitone f :=
  forall_swap

Monotonicity of Composition with Order Dual Equivalence Characterizes Antitone Functions

Informal description

For any function $f : \alpha \to \beta$ between preorders, the composition $f \circ \text{ofDual}$ is monotone if and only if $f$ is antitone. Here, $\text{ofDual} : \alpha^{\text{op}} \to \alpha$ is the identity map that interprets an element of the order dual $\alpha^{\text{op}}$ as an element of $\alpha$.

antitone_comp_ofDual_iff theorem

: Antitone (f ∘ ofDual) ↔ Monotone f

Full source

@[simp]
theorem antitone_comp_ofDual_iff : AntitoneAntitone (f ∘ ofDual) ↔ Monotone f :=
  forall_swap

Antitone Function Composed with Order Dual Identity is Monotone

Informal description

A function $f : \alpha \to \beta$ is antitone (i.e., order-reversing) if and only if the composition $f \circ \text{ofDual}$ is monotone (i.e., order-preserving), where $\text{ofDual} : \alpha^{\text{op}} \to \alpha$ is the identity map from the order dual of $\alpha$ to $\alpha$ itself.

monotone_toDual_comp_iff theorem

: Monotone (toDual ∘ f : α → βᵒᵈ) ↔ Antitone f

Full source

@[simp]
theorem monotone_toDual_comp_iff : MonotoneMonotone (toDual ∘ f : α → βᵒᵈ) ↔ Antitone f :=
  Iff.rfl

Monotonicity of Dual Composition $\leftrightarrow$ Antitonicity of Original Function

Informal description

For a function $f : \alpha \to \beta$ between preorders, the composition of $f$ with the order dual map $\text{toDual} : \beta \to \beta^{\text{op}}$ is monotone if and only if $f$ is antitone. In other words, the following are equivalent: 1. The map $\text{toDual} \circ f : \alpha \to \beta^{\text{op}}$ is monotone. 2. The function $f$ is antitone (i.e., $a \leq b$ implies $f(b) \leq f(a)$ for all $a, b \in \alpha$).

antitone_toDual_comp_iff theorem

: Antitone (toDual ∘ f : α → βᵒᵈ) ↔ Monotone f

Full source

@[simp]
theorem antitone_toDual_comp_iff : AntitoneAntitone (toDual ∘ f : α → βᵒᵈ) ↔ Monotone f :=
  Iff.rfl

Monotonicity of $f$ is equivalent to antitonicity of $\text{toDual} \circ f$

Informal description

A function $f : \alpha \to \beta$ between preorders is monotone if and only if the composition of $f$ with the order dual embedding $\text{toDual} : \beta \to \beta^{\text{op}}$ is antitone. In other words, $f$ is monotone precisely when $\text{toDual} \circ f : \alpha \to \beta^{\text{op}}$ is antitone.

monotoneOn_comp_ofDual_iff theorem

: MonotoneOn (f ∘ ofDual) s ↔ AntitoneOn f s

Full source

@[simp]
theorem monotoneOn_comp_ofDual_iff : MonotoneOnMonotoneOn (f ∘ ofDual) s ↔ AntitoneOn f s :=
  forall₂_swap

Monotonicity of Composition with Dual Order Map Equivalence: $f \circ \text{ofDual}$ Monotone $\leftrightarrow$ $f$ Antitone

Informal description

For any function $f \colon \alpha \to \beta$ between preorders and any subset $s \subseteq \alpha$, the composition $f \circ \text{ofDual}$ is monotone on $s$ if and only if $f$ is antitone on $s$. Here, $\text{ofDual} \colon \alpha^{\text{op}} \to \alpha$ is the identity map from the order dual of $\alpha$ to $\alpha$ itself.

antitoneOn_comp_ofDual_iff theorem

: AntitoneOn (f ∘ ofDual) s ↔ MonotoneOn f s

Full source

@[simp]
theorem antitoneOn_comp_ofDual_iff : AntitoneOnAntitoneOn (f ∘ ofDual) s ↔ MonotoneOn f s :=
  forall₂_swap

Antitone Composition with Order Dual Implies Monotonicity

Informal description

For a function $f \colon \alpha \to \beta$ between preorders and a subset $s \subseteq \alpha$, the composition $f \circ \text{ofDual}$ is antitone on $s$ if and only if $f$ is monotone on $s$. Here, $\text{ofDual} \colon \alpha^{\text{op}} \to \alpha$ is the identity map from the order dual of $\alpha$ to $\alpha$ itself.

monotoneOn_toDual_comp_iff theorem

: MonotoneOn (toDual ∘ f : α → βᵒᵈ) s ↔ AntitoneOn f s

Full source

@[simp]
theorem monotoneOn_toDual_comp_iff : MonotoneOnMonotoneOn (toDual ∘ f : α → βᵒᵈ) s ↔ AntitoneOn f s :=
  Iff.rfl

Monotonicity of Order Dual Composition Equivalence: $\text{toDual} \circ f$ Monotone $\leftrightarrow$ $f$ Antitone

Informal description

For a function $f \colon \alpha \to \beta$ between preorders and a subset $s \subseteq \alpha$, the composition of $f$ with the order dual map $\text{toDual} \colon \beta \to \beta^{\text{op}}$ is monotone on $s$ if and only if $f$ is antitone on $s$. In other words, the following are equivalent: 1. The function $\text{toDual} \circ f \colon \alpha \to \beta^{\text{op}}$ is monotone on $s$. 2. The function $f \colon \alpha \to \beta$ is antitone on $s$.

antitoneOn_toDual_comp_iff theorem

: AntitoneOn (toDual ∘ f : α → βᵒᵈ) s ↔ MonotoneOn f s

Full source

@[simp]
theorem antitoneOn_toDual_comp_iff : AntitoneOnAntitoneOn (toDual ∘ f : α → βᵒᵈ) s ↔ MonotoneOn f s :=
  Iff.rfl

Monotonicity via Order Dual Composition: $\text{AntitoneOn} (\text{toDual} \circ f) \leftrightarrow \text{MonotoneOn} f$

Informal description

Let $\alpha$ and $\beta$ be preorders, $f \colon \alpha \to \beta$ a function, and $s \subseteq \alpha$ a subset. Then the following are equivalent: 1. The composition of $f$ with the order dual map $\text{toDual} \colon \beta \to \beta^{\text{op}}$ is antitone on $s$. 2. The function $f$ is monotone on $s$. In other words, $f$ composed with the order-reversing embedding is decreasing if and only if $f$ itself is increasing.

strictMono_comp_ofDual_iff theorem

: StrictMono (f ∘ ofDual) ↔ StrictAnti f

Full source

@[simp]
theorem strictMono_comp_ofDual_iff : StrictMonoStrictMono (f ∘ ofDual) ↔ StrictAnti f :=
  forall_swap

Strict Monotonicity of Composition with Dual Order Map iff Strict Antitonicity

Informal description

Let $f : \alpha \to \beta$ be a function between preorders. Then $f \circ \text{ofDual}$ is strictly monotone if and only if $f$ is strictly antitone, where $\text{ofDual} : \alpha^{\text{op}} \to \alpha$ is the identity map from the order dual of $\alpha$ to $\alpha$ itself.

strictAnti_comp_ofDual_iff theorem

: StrictAnti (f ∘ ofDual) ↔ StrictMono f

Full source

@[simp]
theorem strictAnti_comp_ofDual_iff : StrictAntiStrictAnti (f ∘ ofDual) ↔ StrictMono f :=
  forall_swap

Strict Antitonicity of Composition with Order Dual Implies Strict Monotonicity

Informal description

For any function $f : \alpha \to \beta$ between preorders, the composition $f \circ \text{ofDual}$ is strictly antitone if and only if $f$ is strictly monotone. Here, $\text{ofDual} : \alpha^{\text{op}} \to \alpha$ is the identity map from the order dual of $\alpha$ to $\alpha$ itself.

strictMono_toDual_comp_iff theorem

: StrictMono (toDual ∘ f : α → βᵒᵈ) ↔ StrictAnti f

Full source

@[simp]
theorem strictMono_toDual_comp_iff : StrictMonoStrictMono (toDual ∘ f : α → βᵒᵈ) ↔ StrictAnti f :=
  Iff.rfl

Strict Monotonicity of Dual Composition Characterizes Strict Antitonicity

Informal description

Let $f : \alpha \to \beta$ be a function between preorders. Then the composition of $f$ with the order dual map $\text{toDual} : \beta \to \beta^{\text{op}}$ is strictly monotone if and only if $f$ is strictly antitone. In other words, the following are equivalent: 1. The function $\text{toDual} \circ f : \alpha \to \beta^{\text{op}}$ is strictly monotone. 2. The function $f : \alpha \to \beta$ is strictly antitone.

strictAnti_toDual_comp_iff theorem

: StrictAnti (toDual ∘ f : α → βᵒᵈ) ↔ StrictMono f

Full source

@[simp]
theorem strictAnti_toDual_comp_iff : StrictAntiStrictAnti (toDual ∘ f : α → βᵒᵈ) ↔ StrictMono f :=
  Iff.rfl

Equivalence of Strict Monotonicity and Strict Antitonicity under Order Dual Composition

Informal description

For a function $f : \alpha \to \beta$ between preorders, the composition of $f$ with the order dual embedding $\text{toDual} : \beta \to \beta^{\text{op}}$ is strictly antitone if and only if $f$ is strictly monotone. In other words, the following equivalence holds: $$ \text{StrictAnti} (\text{toDual} \circ f) \leftrightarrow \text{StrictMono} f $$ where $\text{StrictAnti}$ denotes strict antitone functions and $\text{StrictMono}$ denotes strictly monotone functions.

strictMonoOn_comp_ofDual_iff theorem

: StrictMonoOn (f ∘ ofDual) s ↔ StrictAntiOn f s

Full source

@[simp]
theorem strictMonoOn_comp_ofDual_iff : StrictMonoOnStrictMonoOn (f ∘ ofDual) s ↔ StrictAntiOn f s :=
  forall₂_swap

Strict Monotonicity of Composition with Order Dual Equivalence to Strict Antitonicity

Informal description

For a function $f : \alpha \to \beta$ between preorders and a subset $s \subseteq \alpha$, the composition $f \circ \text{ofDual}$ is strictly monotone on $s$ if and only if $f$ is strictly antitone on $s$. Here, $\text{ofDual} : \alpha^{\text{op}} \to \alpha$ is the identity map from the order dual of $\alpha$ to $\alpha$ itself.

strictAntiOn_comp_ofDual_iff theorem

: StrictAntiOn (f ∘ ofDual) s ↔ StrictMonoOn f s

Full source

@[simp]
theorem strictAntiOn_comp_ofDual_iff : StrictAntiOnStrictAntiOn (f ∘ ofDual) s ↔ StrictMonoOn f s :=
  forall₂_swap

Strict Antitonicity of Composition with Order Dual Implies Strict Monotonicity

Informal description

For a function $f : \alpha \to \beta$ between preorders and a subset $s \subseteq \alpha$, the composition $f \circ \text{ofDual}$ is strictly antitone on $s$ if and only if $f$ is strictly monotone on $s$. Here, $\text{ofDual} : \alpha^{\text{op}} \to \alpha$ is the identity map from the order dual of $\alpha$ to $\alpha$.

strictMonoOn_toDual_comp_iff theorem

: StrictMonoOn (toDual ∘ f : α → βᵒᵈ) s ↔ StrictAntiOn f s

Full source

@[simp]
theorem strictMonoOn_toDual_comp_iff : StrictMonoOnStrictMonoOn (toDual ∘ f : α → βᵒᵈ) s ↔ StrictAntiOn f s :=
  Iff.rfl

Strict Monotonicity of Dual Composition Equivalence: $\text{toDual} \circ f$ Strictly Monotone on $s$ $\iff$ $f$ Strictly Antitone on $s$

Informal description

Let $f : \alpha \to \beta$ be a function between preorders, and let $s \subseteq \alpha$. The composition of $f$ with the order dual map $\text{toDual} : \beta \to \beta^{\text{op}}$ is strictly monotone on $s$ if and only if $f$ is strictly antitone on $s$. In other words, the following are equivalent: 1. The function $\text{toDual} \circ f : \alpha \to \beta^{\text{op}}$ is strictly monotone on $s$. 2. The function $f$ is strictly antitone on $s$.

strictAntiOn_toDual_comp_iff theorem

: StrictAntiOn (toDual ∘ f : α → βᵒᵈ) s ↔ StrictMonoOn f s

Full source

@[simp]
theorem strictAntiOn_toDual_comp_iff : StrictAntiOnStrictAntiOn (toDual ∘ f : α → βᵒᵈ) s ↔ StrictMonoOn f s :=
  Iff.rfl

Strict Antitonicity of Dual Composition Equivalent to Strict Monotonicity

Informal description

For a function $f : \alpha \to \beta$ between preorders and a subset $s \subseteq \alpha$, the composition of $f$ with the order dual map $\text{toDual} : \beta \to \beta^{\text{op}}$ is strictly antitone on $s$ if and only if $f$ is strictly monotone on $s$. In other words, the following are equivalent: 1. The map $\text{toDual} \circ f : \alpha \to \beta^{\text{op}}$ satisfies $f(b) < f(a)$ for all $a, b \in s$ with $a < b$. 2. The original function $f : \alpha \to \beta$ satisfies $f(a) < f(b)$ for all $a, b \in s$ with $a < b$.

monotone_dual_iff theorem

: Monotone (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) ↔ Monotone f

Full source

theorem monotone_dual_iff : MonotoneMonotone (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) ↔ Monotone f := by
  rw [monotone_toDual_comp_iff, antitone_comp_ofDual_iff]

Monotonicity of Dual Composition $\leftrightarrow$ Monotonicity of Original Function

Informal description

For a function $f : \alpha \to \beta$ between preorders, the composition $\text{toDual} \circ f \circ \text{ofDual} : \alpha^{\text{op}} \to \beta^{\text{op}}$ is monotone if and only if $f$ is monotone. Here, $\text{toDual} : \beta \to \beta^{\text{op}}$ and $\text{ofDual} : \alpha^{\text{op}} \to \alpha$ are the identity maps to and from the order duals, respectively.

antitone_dual_iff theorem

: Antitone (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) ↔ Antitone f

Full source

theorem antitone_dual_iff : AntitoneAntitone (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) ↔ Antitone f := by
  rw [antitone_toDual_comp_iff, monotone_comp_ofDual_iff]

Antitonicity of $f$ is equivalent to antitonicity of its dual composition

Informal description

For a function $f : \alpha \to \beta$ between preorders, the composition $\text{toDual} \circ f \circ \text{ofDual} : \alpha^{\text{op}} \to \beta^{\text{op}}$ is antitone if and only if $f$ is antitone. Here, $\text{toDual} : \beta \to \beta^{\text{op}}$ and $\text{ofDual} : \alpha^{\text{op}} \to \alpha$ are the order dual identity maps.

monotoneOn_dual_iff theorem

: MonotoneOn (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) s ↔ MonotoneOn f s

Full source

theorem monotoneOn_dual_iff : MonotoneOnMonotoneOn (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) s ↔ MonotoneOn f s := by
  rw [monotoneOn_toDual_comp_iff, antitoneOn_comp_ofDual_iff]

Monotonicity Equivalence via Order Dual Composition

Informal description

For a function $f \colon \alpha \to \beta$ between preorders and a subset $s \subseteq \alpha$, the composition $\text{toDual} \circ f \circ \text{ofDual} \colon \alpha^{\text{op}} \to \beta^{\text{op}}$ is monotone on $s$ if and only if $f$ is monotone on $s$. Here, $\text{toDual} \colon \beta \to \beta^{\text{op}}$ and $\text{ofDual} \colon \alpha^{\text{op}} \to \alpha$ are the canonical order-reversing bijections.

antitoneOn_dual_iff theorem

: AntitoneOn (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) s ↔ AntitoneOn f s

Full source

theorem antitoneOn_dual_iff : AntitoneOnAntitoneOn (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) s ↔ AntitoneOn f s := by
  rw [antitoneOn_toDual_comp_iff, monotoneOn_comp_ofDual_iff]

Antitonicity via Order Dual Composition: $\text{AntitoneOn} (\text{toDual} \circ f \circ \text{ofDual}) \leftrightarrow \text{AntitoneOn} f$

Informal description

Let $\alpha$ and $\beta$ be preorders, $f \colon \alpha \to \beta$ a function, and $s \subseteq \alpha$ a subset. Then the following are equivalent: 1. The composition $\text{toDual} \circ f \circ \text{ofDual} \colon \alpha^{\text{op}} \to \beta^{\text{op}}$ is antitone on $s$. 2. The function $f$ is antitone on $s$. Here, $\text{toDual} \colon \beta \to \beta^{\text{op}}$ and $\text{ofDual} \colon \alpha^{\text{op}} \to \alpha$ are the canonical order-reversing bijections between a type and its order dual.

strictMono_dual_iff theorem

: StrictMono (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) ↔ StrictMono f

Full source

theorem strictMono_dual_iff : StrictMonoStrictMono (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) ↔ StrictMono f := by
  rw [strictMono_toDual_comp_iff, strictAnti_comp_ofDual_iff]

Strict Monotonicity of Dual Composition Characterizes Strict Monotonicity of $f$

Informal description

Let $f : \alpha \to \beta$ be a function between preorders. Then the composition $\text{toDual} \circ f \circ \text{ofDual} : \alpha^{\text{op}} \to \beta^{\text{op}}$ is strictly monotone if and only if $f$ is strictly monotone. Here, $\text{toDual} : \beta \to \beta^{\text{op}}$ and $\text{ofDual} : \alpha^{\text{op}} \to \alpha$ are the order dual maps.

strictAnti_dual_iff theorem

: StrictAnti (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) ↔ StrictAnti f

Full source

theorem strictAnti_dual_iff : StrictAntiStrictAnti (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) ↔ StrictAnti f := by
  rw [strictAnti_toDual_comp_iff, strictMono_comp_ofDual_iff]

Strict Antitonicity under Order Dual Composition $\leftrightarrow$ Strict Antitonicity

Informal description

For a function $f \colon \alpha \to \beta$ between preorders, the composition $\text{toDual} \circ f \circ \text{ofDual} \colon \alpha^{\text{op}} \to \beta^{\text{op}}$ is strictly antitone if and only if $f$ is strictly antitone. Here, $\text{toDual} \colon \beta \to \beta^{\text{op}}$ and $\text{ofDual} \colon \alpha^{\text{op}} \to \alpha$ are the canonical order-reversing bijections.

strictMonoOn_dual_iff theorem

: StrictMonoOn (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) s ↔ StrictMonoOn f s

Full source

theorem strictMonoOn_dual_iff :
    StrictMonoOnStrictMonoOn (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) s ↔ StrictMonoOn f s := by
  rw [strictMonoOn_toDual_comp_iff, strictAntiOn_comp_ofDual_iff]

Strict Monotonicity of Dual Composition Equivalence: $\text{toDual} \circ f \circ \text{ofDual}$ Strictly Monotone on $s$ $\iff$ $f$ Strictly Monotone on $s$

Informal description

Let $f : \alpha \to \beta$ be a function between preorders, and let $s \subseteq \alpha$. The composition $\text{toDual} \circ f \circ \text{ofDual} : \alpha^{\text{op}} \to \beta^{\text{op}}$ is strictly monotone on $s$ if and only if $f$ is strictly monotone on $s$. Here, $\text{toDual} : \beta \to \beta^{\text{op}}$ and $\text{ofDual} : \alpha^{\text{op}} \to \alpha$ are the order dual maps.

strictAntiOn_dual_iff theorem

: StrictAntiOn (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) s ↔ StrictAntiOn f s

Full source

theorem strictAntiOn_dual_iff :
    StrictAntiOnStrictAntiOn (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) s ↔ StrictAntiOn f s := by
  rw [strictAntiOn_toDual_comp_iff, strictMonoOn_comp_ofDual_iff]

Strict Antitonicity of Dual Composition $\leftrightarrow$ Strict Antitonicity on Subset

Informal description

For a function $f \colon \alpha \to \beta$ between preorders and a subset $s \subseteq \alpha$, the composition $\text{toDual} \circ f \circ \text{ofDual} \colon \alpha^{\text{op}} \to \beta^{\text{op}}$ is strictly antitone on $s$ if and only if $f$ is strictly antitone on $s$. Here, $\text{toDual} \colon \beta \to \beta^{\text{op}}$ and $\text{ofDual} \colon \alpha^{\text{op}} \to \alpha$ are the canonical order-reversing bijections.

StrictMono.wellFoundedLT theorem

[WellFoundedLT β] (hf : StrictMono f) : WellFoundedLT α

Full source

theorem StrictMono.wellFoundedLT [WellFoundedLT β] (hf : StrictMono f) : WellFoundedLT α :=
  Subrelation.isWellFounded (InvImage (· < ·) f) @hf

Well-foundedness of strict order under strictly monotone functions

Informal description

Let $\alpha$ and $\beta$ be types with strict less-than relations, and suppose $\beta$ has a well-founded strict less-than relation. If $f : \alpha \to \beta$ is a strictly monotone function, then $\alpha$ also has a well-founded strict less-than relation.

StrictAnti.wellFoundedLT theorem

[WellFoundedGT β] (hf : StrictAnti f) : WellFoundedLT α

Full source

theorem StrictAnti.wellFoundedLT [WellFoundedGT β] (hf : StrictAnti f) : WellFoundedLT α :=
  StrictMono.wellFoundedLT (β := βᵒᵈ) hf

Well-foundedness of strict less-than order under strictly antitone functions

Informal description

Let $\alpha$ and $\beta$ be preordered types, and suppose $\beta$ has a well-founded "greater than" relation. If $f : \alpha \to \beta$ is a strictly antitone function, then $\alpha$ has a well-founded "less than" relation.

StrictMono.wellFoundedGT theorem

[WellFoundedGT β] (hf : StrictMono f) : WellFoundedGT α

Full source

theorem StrictMono.wellFoundedGT [WellFoundedGT β] (hf : StrictMono f) : WellFoundedGT α :=
  StrictMono.wellFoundedLT (α := αᵒᵈ) (β := βᵒᵈ) (fun _ _ h ↦ hf h)

Well-foundedness of "greater than" under strictly monotone functions

Informal description

Let $\alpha$ and $\beta$ be preordered types, and suppose $\beta$ has a well-founded "greater than" relation. If $f : \alpha \to \beta$ is a strictly monotone function, then $\alpha$ also has a well-founded "greater than" relation.

StrictAnti.wellFoundedGT theorem

[WellFoundedLT β] (hf : StrictAnti f) : WellFoundedGT α

Full source

theorem StrictAnti.wellFoundedGT [WellFoundedLT β] (hf : StrictAnti f) : WellFoundedGT α :=
  StrictMono.wellFoundedLT (α := αᵒᵈ) (fun _ _ h ↦ hf h)

Well-foundedness of strict greater-than order under strictly antitone functions

Informal description

Let $\alpha$ and $\beta$ be types with strict orders, and suppose $\beta$ has a well-founded strict less-than relation. If $f : \alpha \to \beta$ is a strictly antitone function, then $\alpha$ has a well-founded strict greater-than relation.

StrictMono.isMax_of_apply theorem

(hf : StrictMono f) (ha : IsMax (f a)) : IsMax a

Full source

theorem StrictMono.isMax_of_apply (hf : StrictMono f) (ha : IsMax (f a)) : IsMax a :=
  of_not_not fun h ↦
    let ⟨_, hb⟩ := not_isMax_iff.1 h
    (hf hb).not_isMax ha

Maximality Preservation under Strictly Monotone Functions

Informal description

Let $f : \alpha \to \beta$ be a strictly monotone function between preorders. If $f(a)$ is a maximal element in $\beta$, then $a$ is a maximal element in $\alpha$.

StrictMono.isMin_of_apply theorem

(hf : StrictMono f) (ha : IsMin (f a)) : IsMin a

Full source

theorem StrictMono.isMin_of_apply (hf : StrictMono f) (ha : IsMin (f a)) : IsMin a :=
  of_not_not fun h ↦
    let ⟨_, hb⟩ := not_isMin_iff.1 h
    (hf hb).not_isMin ha

Minimality Preservation under Strictly Monotone Functions

Informal description

Let $f : \alpha \to \beta$ be a strictly monotone function between preorders. If $f(a)$ is a minimal element in $\beta$, then $a$ is a minimal element in $\alpha$.

StrictAnti.isMax_of_apply theorem

(hf : StrictAnti f) (ha : IsMin (f a)) : IsMax a

Full source

theorem StrictAnti.isMax_of_apply (hf : StrictAnti f) (ha : IsMin (f a)) : IsMax a :=
  of_not_not fun h ↦
    let ⟨_, hb⟩ := not_isMax_iff.1 h
    (hf hb).not_isMin ha

Maximality from Minimality under Strictly Antitone Functions

Informal description

Let $f : \alpha \to \beta$ be a strictly antitone function between preorders, and let $a \in \alpha$. If $f(a)$ is a minimal element in $\beta$, then $a$ is a maximal element in $\alpha$.

StrictAnti.isMin_of_apply theorem

(hf : StrictAnti f) (ha : IsMax (f a)) : IsMin a

Full source

theorem StrictAnti.isMin_of_apply (hf : StrictAnti f) (ha : IsMax (f a)) : IsMin a :=
  of_not_not fun h ↦
    let ⟨_, hb⟩ := not_isMin_iff.1 h
    (hf hb).not_isMax ha

Minimality from Maximality under Strictly Antitone Functions

Informal description

Let $f : \alpha \to \beta$ be a strictly antitone function between preorders, and let $a \in \alpha$. If $f(a)$ is a maximal element in $\beta$, then $a$ is a minimal element in $\alpha$.

StrictMono.add_le_nat theorem

{f : ℕ → ℕ} (hf : StrictMono f) (m n : ℕ) : m + f n ≤ f (m + n)

Full source

lemma StrictMono.add_le_nat {f : ℕ → ℕ} (hf : StrictMono f) (m n : ℕ) : m + f n ≤ f (m + n)  := by
  rw [Nat.add_comm m, Nat.add_comm m]
  induction m with
  | zero => rw [Nat.add_zero, Nat.add_zero]
  | succ m ih =>
    rw [← Nat.add_assoc, ← Nat.add_assoc, Nat.succ_le]
    exact ih.trans_lt (hf (n + m).lt_succ_self)

Additive Inequality for Strictly Increasing Functions on Natural Numbers

Informal description

For any strictly increasing function $f \colon \mathbb{N} \to \mathbb{N}$ and any natural numbers $m, n \in \mathbb{N}$, we have $m + f(n) \leq f(m + n)$.

StrictMono.ite' theorem

 (hf : StrictMono f) (hg : StrictMono g) {p : α → Prop} [DecidablePred p] (hp : ∀ ⦃x y⦄, x < y → p y → p x)
  (hfg : ∀ ⦃x y⦄, p x → ¬p y → x < y → f x < g y) : StrictMono fun x ↦ if p x then f x else g x

Full source

protected theorem StrictMono.ite' (hf : StrictMono f) (hg : StrictMono g) {p : α → Prop}
    [DecidablePred p]
    (hp : ∀ ⦃x y⦄, x < y → p y → p x) (hfg : ∀ ⦃x y⦄, p x → ¬p y → x < y → f x < g y) :
    StrictMono fun x ↦ if p x then f x else g x := by
  intro x y h
  by_cases hy : p y
  · have hx : p x := hp h hy
    simpa [hx, hy] using hf h
  by_cases hx : p x
  · simpa [hx, hy] using hfg hx hy h
  · simpa [hx, hy] using hg h

Strict Monotonicity of Piecewise Function with Predicate Condition

Informal description

Let $f$ and $g$ be strictly monotone functions from a preorder $\alpha$ to a preorder $\beta$, and let $p$ be a predicate on $\alpha$ such that for any $x < y$, if $p(y)$ holds then $p(x)$ holds. Suppose further that for any $x < y$ with $p(x)$ and $\neg p(y)$, we have $f(x) < g(y)$. Then the function defined by \[ h(x) = \begin{cases} f(x) & \text{if } p(x), \\ g(x) & \text{otherwise} \end{cases} \] is strictly monotone.

StrictMono.ite theorem

 (hf : StrictMono f) (hg : StrictMono g) {p : α → Prop} [DecidablePred p] (hp : ∀ ⦃x y⦄, x < y → p y → p x)
  (hfg : ∀ x, f x ≤ g x) : StrictMono fun x ↦ if p x then f x else g x

Full source

protected theorem StrictMono.ite (hf : StrictMono f) (hg : StrictMono g) {p : α → Prop}
    [DecidablePred p] (hp : ∀ ⦃x y⦄, x < y → p y → p x) (hfg : ∀ x, f x ≤ g x) :
    StrictMono fun x ↦ if p x then f x else g x :=
  (hf.ite' hg hp) fun _ y _ _ h ↦ (hf h).trans_le (hfg y)

Strict Monotonicity of Piecewise Function with Dominance Condition

Informal description

Let $f$ and $g$ be strictly monotone functions from a preorder $\alpha$ to a preorder $\beta$, and let $p$ be a decidable predicate on $\alpha$ such that for any $x < y$, if $p(y)$ holds then $p(x)$ holds. Suppose further that $f(x) \leq g(x)$ for all $x \in \alpha$. Then the piecewise function defined by \[ h(x) = \begin{cases} f(x) & \text{if } p(x), \\ g(x) & \text{otherwise} \end{cases} \] is strictly monotone.

StrictAnti.ite' theorem

 (hf : StrictAnti f) (hg : StrictAnti g) {p : α → Prop} [DecidablePred p] (hp : ∀ ⦃x y⦄, x < y → p y → p x)
  (hfg : ∀ ⦃x y⦄, p x → ¬p y → x < y → g y < f x) : StrictAnti fun x ↦ if p x then f x else g x

Full source

protected theorem StrictAnti.ite' (hf : StrictAnti f) (hg : StrictAnti g) {p : α → Prop}
    [DecidablePred p]
    (hp : ∀ ⦃x y⦄, x < y → p y → p x) (hfg : ∀ ⦃x y⦄, p x → ¬p y → x < y → g y < f x) :
    StrictAnti fun x ↦ if p x then f x else g x :=
  StrictMono.ite' hf.dual_right hg.dual_right hp hfg

Strict Antitonicity of Predicate-Conditioned Piecewise Function

Informal description

Let $f$ and $g$ be strictly antitone functions from a preorder $\alpha$ to a preorder $\beta$, and let $p$ be a decidable predicate on $\alpha$ such that for any $x < y$, if $p(y)$ holds then $p(x)$ holds. Suppose further that for any $x < y$ with $p(x)$ and $\neg p(y)$, we have $g(y) < f(x)$. Then the piecewise function defined by \[ h(x) = \begin{cases} f(x) & \text{if } p(x), \\ g(x) & \text{otherwise} \end{cases} \] is strictly antitone.

StrictAnti.ite theorem

 (hf : StrictAnti f) (hg : StrictAnti g) {p : α → Prop} [DecidablePred p] (hp : ∀ ⦃x y⦄, x < y → p y → p x)
  (hfg : ∀ x, g x ≤ f x) : StrictAnti fun x ↦ if p x then f x else g x

Full source

protected theorem StrictAnti.ite (hf : StrictAnti f) (hg : StrictAnti g) {p : α → Prop}
    [DecidablePred p] (hp : ∀ ⦃x y⦄, x < y → p y → p x) (hfg : ∀ x, g x ≤ f x) :
    StrictAnti fun x ↦ if p x then f x else g x :=
  (hf.ite' hg hp) fun _ y _ _ h ↦ (hfg y).trans_lt (hf h)

Strict Antitonicity of Dominated Piecewise Function

Informal description

Let $f$ and $g$ be strictly antitone functions from a preorder $\alpha$ to a preorder $\beta$, and let $p$ be a decidable predicate on $\alpha$ such that for any $x < y$, if $p(y)$ holds then $p(x)$ holds. Suppose further that $g(x) \leq f(x)$ for all $x \in \alpha$. Then the piecewise function defined by \[ h(x) = \begin{cases} f(x) & \text{if } p(x), \\ g(x) & \text{otherwise} \end{cases} \] is strictly antitone.

List.foldl_monotone theorem

 [Preorder α] {f : α → β → α} (H : ∀ b, Monotone fun a ↦ f a b) (l : List β) : Monotone fun a ↦ l.foldl f a

Full source

theorem foldl_monotone [Preorder α] {f : α → β → α} (H : ∀ b, Monotone fun a ↦ f a b)
    (l : List β) : Monotone fun a ↦ l.foldl f a :=
  List.recOn l (fun _ _ ↦ id) fun _ _ hl _ _ h ↦ hl (H _ h)

Monotonicity of Left Fold with Monotone Step Function

Informal description

Let $\alpha$ be a type with a preorder and $\beta$ be any type. Given a function $f : \alpha \to \beta \to \alpha$ such that for every $b \in \beta$, the function $\lambda a \mapsto f(a, b)$ is monotone, then for any list $l$ of elements of $\beta$, the function $\lambda a \mapsto \text{foldl } f \, a \, l$ is monotone.

List.foldr_monotone theorem

[Preorder β] {f : α → β → β} (H : ∀ a, Monotone (f a)) (l : List α) : Monotone fun b ↦ l.foldr f b

Full source

theorem foldr_monotone [Preorder β] {f : α → β → β} (H : ∀ a, Monotone (f a)) (l : List α) :
    Monotone fun b ↦ l.foldr f b := fun _ _ h ↦ List.recOn l h fun i _ hl ↦ H i hl

Monotonicity of Right Fold with Monotone Step Function

Informal description

Let $\beta$ be a type with a preorder, and let $f : \alpha \to \beta \to \beta$ be a function such that for each $a \in \alpha$, the function $f(a)$ is monotone. Then for any list $l$ of elements of $\alpha$, the function $\lambda b \mapsto \text{foldr } f \, b \, l$ is monotone.

List.foldl_strictMono theorem

 [Preorder α] {f : α → β → α} (H : ∀ b, StrictMono fun a ↦ f a b) (l : List β) : StrictMono fun a ↦ l.foldl f a

Full source

theorem foldl_strictMono [Preorder α] {f : α → β → α} (H : ∀ b, StrictMono fun a ↦ f a b)
    (l : List β) : StrictMono fun a ↦ l.foldl f a :=
  List.recOn l (fun _ _ ↦ id) fun _ _ hl _ _ h ↦ hl (H _ h)

Strict Monotonicity of Left Fold with Strictly Monotone Step Function

Informal description

Let $\alpha$ be a type with a preorder and $\beta$ be any type. Given a function $f : \alpha \to \beta \to \alpha$ such that for every $b \in \beta$, the function $\lambda a \mapsto f(a, b)$ is strictly monotone, then for any list $l$ of elements of $\beta$, the function $\lambda a \mapsto \text{foldl } f \, a \, l$ is strictly monotone.

List.foldr_strictMono theorem

[Preorder β] {f : α → β → β} (H : ∀ a, StrictMono (f a)) (l : List α) : StrictMono fun b ↦ l.foldr f b

Full source

theorem foldr_strictMono [Preorder β] {f : α → β → β} (H : ∀ a, StrictMono (f a)) (l : List α) :
    StrictMono fun b ↦ l.foldr f b := fun _ _ h ↦ List.recOn l h fun i _ hl ↦ H i hl

Strict Monotonicity of Right Fold with Strictly Monotone Step Function

Informal description

Let $\beta$ be a type with a preorder and let $f : \alpha \to \beta \to \beta$ be a function such that for every $a \in \alpha$, the function $f(a)$ is strictly monotone. Then for any list $l$ of elements of $\alpha$, the function $b \mapsto \text{foldr } f \, b \, l$ is strictly monotone.

StrictMonoOn.le_iff_le theorem

(hf : StrictMonoOn f s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) : f a ≤ f b ↔ a ≤ b

Full source

theorem StrictMonoOn.le_iff_le (hf : StrictMonoOn f s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) :
    f a ≤ f b ↔ a ≤ b :=
  ⟨fun h ↦ le_of_not_gt fun h' ↦ (hf hb ha h').not_le h, fun h ↦
    h.lt_or_eq_dec.elim (fun h' ↦ (hf ha hb h').le) fun h' ↦ h' ▸ le_rfl⟩

Strictly Monotone Function Preserves Order on Subset: $f(a) \leq f(b) \leftrightarrow a \leq b$

Informal description

Let $f : \alpha \to \beta$ be a strictly monotone function on a subset $s \subseteq \alpha$ (i.e., for any $a, b \in s$, $a < b$ implies $f(a) < f(b)$). Then for any $a, b \in s$, we have $f(a) \leq f(b)$ if and only if $a \leq b$.

StrictAntiOn.le_iff_le theorem

(hf : StrictAntiOn f s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) : f a ≤ f b ↔ b ≤ a

Full source

theorem StrictAntiOn.le_iff_le (hf : StrictAntiOn f s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) :
    f a ≤ f b ↔ b ≤ a :=
  hf.dual_right.le_iff_le hb ha

Strictly Antitone Function Reverses Order on Subset: $f(a) \leq f(b) \leftrightarrow b \leq a$

Informal description

Let $f : \alpha \to \beta$ be a strictly antitone function on a subset $s \subseteq \alpha$ (i.e., for any $a, b \in s$, $a < b$ implies $f(b) < f(a)$). Then for any $a, b \in s$, we have $f(a) \leq f(b)$ if and only if $b \leq a$.

StrictMonoOn.lt_iff_lt theorem

(hf : StrictMonoOn f s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) : f a < f b ↔ a < b

Full source

theorem StrictMonoOn.lt_iff_lt (hf : StrictMonoOn f s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) :
    f a < f b ↔ a < b := by
  rw [lt_iff_le_not_le, lt_iff_le_not_le, hf.le_iff_le ha hb, hf.le_iff_le hb ha]

Strictly Monotone Function Preserves Strict Order on Subset: $f(a) < f(b) \leftrightarrow a < b$

Informal description

Let $f : \alpha \to \beta$ be a strictly monotone function on a subset $s \subseteq \alpha$ (i.e., for any $x, y \in s$, $x < y$ implies $f(x) < f(y)$). Then for any $a, b \in s$, we have $f(a) < f(b)$ if and only if $a < b$.

StrictAntiOn.lt_iff_lt theorem

(hf : StrictAntiOn f s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) : f a < f b ↔ b < a

Full source

theorem StrictAntiOn.lt_iff_lt (hf : StrictAntiOn f s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) :
    f a < f b ↔ b < a :=
  hf.dual_right.lt_iff_lt hb ha

Strictly Antitone Function Reverses Strict Order on Subset: $f(a) < f(b) \leftrightarrow b < a$

Informal description

Let $f : \alpha \to \beta$ be a strictly antitone function on a subset $s \subseteq \alpha$ (i.e., for any $x, y \in s$, $x < y$ implies $f(y) < f(x)$). Then for any $a, b \in s$, we have $f(a) < f(b)$ if and only if $b < a$.

StrictMono.le_iff_le theorem

(hf : StrictMono f) {a b : α} : f a ≤ f b ↔ a ≤ b

Full source

theorem StrictMono.le_iff_le (hf : StrictMono f) {a b : α} : f a ≤ f b ↔ a ≤ b :=
  (hf.strictMonoOn Set.univ).le_iff_le trivial trivial

Strictly Monotone Function Preserves Order: $f(a) \leq f(b) \leftrightarrow a \leq b$

Informal description

Let $f : \alpha \to \beta$ be a strictly monotone function between two preorders. Then for any $a, b \in \alpha$, we have $f(a) \leq f(b)$ if and only if $a \leq b$.

StrictAnti.le_iff_le theorem

(hf : StrictAnti f) {a b : α} : f a ≤ f b ↔ b ≤ a

Full source

theorem StrictAnti.le_iff_le (hf : StrictAnti f) {a b : α} : f a ≤ f b ↔ b ≤ a :=
  (hf.strictAntiOn Set.univ).le_iff_le trivial trivial

Strictly Antitone Function Reverses Order: $f(a) \leq f(b) \leftrightarrow b \leq a$

Informal description

Let $f : \alpha \to \beta$ be a strictly antitone function between two preorders. Then for any $a, b \in \alpha$, we have $f(a) \leq f(b)$ if and only if $b \leq a$.

StrictMono.lt_iff_lt theorem

(hf : StrictMono f) {a b : α} : f a < f b ↔ a < b

Full source

theorem StrictMono.lt_iff_lt (hf : StrictMono f) {a b : α} : f a < f b ↔ a < b :=
  (hf.strictMonoOn Set.univ).lt_iff_lt trivial trivial

Strictly Monotone Function Preserves Strict Order: $f(a) < f(b) \leftrightarrow a < b$

Informal description

Let $f : \alpha \to \beta$ be a strictly monotone function between two preorders. Then for any $a, b \in \alpha$, we have $f(a) < f(b)$ if and only if $a < b$.

StrictAnti.lt_iff_lt theorem

(hf : StrictAnti f) {a b : α} : f a < f b ↔ b < a

Full source

theorem StrictAnti.lt_iff_lt (hf : StrictAnti f) {a b : α} : f a < f b ↔ b < a :=
  (hf.strictAntiOn Set.univ).lt_iff_lt trivial trivial

Strictly Antitone Function Reverses Strict Order: $f(a) < f(b) \leftrightarrow b < a$

Informal description

Let $f : \alpha \to \beta$ be a strictly antitone function between two preorders. Then for any $a, b \in \alpha$, we have $f(a) < f(b)$ if and only if $b < a$.

StrictMonoOn.compares theorem

 (hf : StrictMonoOn f s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) : ∀ {o : Ordering}, o.Compares (f a) (f b) ↔ o.Compares a b

Full source

protected theorem StrictMonoOn.compares (hf : StrictMonoOn f s) {a b : α} (ha : a ∈ s)
    (hb : b ∈ s) : ∀ {o : Ordering}, o.Compares (f a) (f b) ↔ o.Compares a b
  | Ordering.lt => hf.lt_iff_lt ha hb
  | Ordering.eq => ⟨fun h ↦ ((hf.le_iff_le ha hb).1 h.le).antisymm
                      ((hf.le_iff_le hb ha).1 h.symm.le), congr_arg _⟩
  | Ordering.gt => hf.lt_iff_lt hb ha

Strictly Monotone Function Preserves Ordering Comparisons on Subset: $o(f(a), f(b)) \leftrightarrow o(a, b)$

Informal description

Let $f : \alpha \to \beta$ be a strictly monotone function on a subset $s \subseteq \alpha$ (i.e., for any $x, y \in s$, $x < y$ implies $f(x) < f(y)$). Then for any $a, b \in s$ and any ordering relation $o$, the comparison $o$ holds between $f(a)$ and $f(b)$ if and only if it holds between $a$ and $b$.

StrictAntiOn.compares theorem

 (hf : StrictAntiOn f s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) {o : Ordering} : o.Compares (f a) (f b) ↔ o.Compares b a

Full source

protected theorem StrictAntiOn.compares (hf : StrictAntiOn f s) {a b : α} (ha : a ∈ s)
    (hb : b ∈ s) {o : Ordering} : o.Compares (f a) (f b) ↔ o.Compares b a :=
  toDual_compares_toDual.trans <| hf.dual_right.compares hb ha

Strictly Antitone Function Reverses Ordering Comparisons on Subset: $o(f(a), f(b)) \leftrightarrow o(b, a)$

Informal description

Let $f : \alpha \to \beta$ be a strictly antitone function on a subset $s \subseteq \alpha$ (i.e., for any $x, y \in s$, $x < y$ implies $f(y) < f(x)$). Then for any $a, b \in s$ and any ordering relation $o$, the comparison $o$ holds between $f(a)$ and $f(b)$ if and only if it holds between $b$ and $a$.

StrictMono.compares theorem

(hf : StrictMono f) {a b : α} {o : Ordering} : o.Compares (f a) (f b) ↔ o.Compares a b

Full source

protected theorem StrictMono.compares (hf : StrictMono f) {a b : α} {o : Ordering} :
    o.Compares (f a) (f b) ↔ o.Compares a b :=
  (hf.strictMonoOn Set.univ).compares trivial trivial

Strictly Monotone Function Preserves Ordering Comparisons: $o(f(a), f(b)) \leftrightarrow o(a, b)$

Informal description

Let $f : \alpha \to \beta$ be a strictly monotone function between two preorders. For any elements $a, b \in \alpha$ and any ordering relation $o$, the comparison $o$ holds between $f(a)$ and $f(b)$ if and only if it holds between $a$ and $b$. In other words, $o(f(a), f(b)) \leftrightarrow o(a, b)$.

StrictAnti.compares theorem

(hf : StrictAnti f) {a b : α} {o : Ordering} : o.Compares (f a) (f b) ↔ o.Compares b a

Full source

protected theorem StrictAnti.compares (hf : StrictAnti f) {a b : α} {o : Ordering} :
    o.Compares (f a) (f b) ↔ o.Compares b a :=
  (hf.strictAntiOn Set.univ).compares trivial trivial

Strictly Antitone Function Reverses Ordering Comparisons: $o(f(a), f(b)) \leftrightarrow o(b, a)$

Informal description

Let $f : \alpha \to \beta$ be a strictly antitone function between two preorders. For any elements $a, b \in \alpha$ and any ordering relation $o$, the comparison $o$ holds between $f(a)$ and $f(b)$ if and only if it holds between $b$ and $a$, i.e., $o(f(a), f(b)) \leftrightarrow o(b, a)$.

StrictMono.injective theorem

(hf : StrictMono f) : Injective f

Full source

theorem StrictMono.injective (hf : StrictMono f) : Injective f :=
  fun x y h ↦ show Compares eq x y from hf.compares.1 h

Strictly Monotone Functions are Injective

Informal description

If a function $f : \alpha \to \beta$ between two preorders is strictly monotone, then it is injective. That is, for any $a, b \in \alpha$, if $f(a) = f(b)$, then $a = b$.

StrictAnti.injective theorem

(hf : StrictAnti f) : Injective f

Full source

theorem StrictAnti.injective (hf : StrictAnti f) : Injective f :=
  fun x y h ↦ show Compares eq x y from hf.compares.1 h.symm

Strictly Antitone Functions are Injective

Informal description

If a function $f : \alpha \to \beta$ between two preorders is strictly antitone, then it is injective. That is, for any $a, b \in \alpha$, if $f(a) = f(b)$, then $a = b$.

StrictMono.maximal_of_maximal_image theorem

(hf : StrictMono f) {a} (hmax : ∀ p, p ≤ f a) (x : α) : x ≤ a

Full source

theorem StrictMono.maximal_of_maximal_image (hf : StrictMono f) {a} (hmax : ∀ p, p ≤ f a) (x : α) :
    x ≤ a :=
  hf.le_iff_le.mp (hmax (f x))

Maximality Preservation under Strictly Monotone Functions

Informal description

Let $f : \alpha \to \beta$ be a strictly monotone function between two preorders. If $a \in \alpha$ is such that $f(a)$ is a maximal element in the codomain (i.e., for all $p \in \beta$, $p \leq f(a)$), then $a$ is a maximal element in the domain (i.e., for all $x \in \alpha$, $x \leq a$).

StrictMono.minimal_of_minimal_image theorem

(hf : StrictMono f) {a} (hmin : ∀ p, f a ≤ p) (x : α) : a ≤ x

Full source

theorem StrictMono.minimal_of_minimal_image (hf : StrictMono f) {a} (hmin : ∀ p, f a ≤ p) (x : α) :
    a ≤ x :=
  hf.le_iff_le.mp (hmin (f x))

Minimality Preservation under Strictly Monotone Functions

Informal description

Let $f : \alpha \to \beta$ be a strictly monotone function between two preorders. If $a \in \alpha$ is such that $f(a)$ is a minimal element in $\beta$ (i.e., $f(a) \leq p$ for all $p \in \beta$), then $a$ is a minimal element in $\alpha$ (i.e., $a \leq x$ for all $x \in \alpha$).

StrictAnti.minimal_of_maximal_image theorem

(hf : StrictAnti f) {a} (hmax : ∀ p, p ≤ f a) (x : α) : a ≤ x

Full source

theorem StrictAnti.minimal_of_maximal_image (hf : StrictAnti f) {a} (hmax : ∀ p, p ≤ f a) (x : α) :
    a ≤ x :=
  hf.le_iff_le.mp (hmax (f x))

Minimality from Maximal Image under Strictly Antitone Function

Informal description

Let $f : \alpha \to \beta$ be a strictly antitone function between two preorders. If $a \in \alpha$ is such that $f(a)$ is a maximal element in $\beta$ (i.e., $p \leq f(a)$ for all $p \in \beta$), then $a$ is a minimal element in $\alpha$ (i.e., $a \leq x$ for all $x \in \alpha$).

StrictAnti.maximal_of_minimal_image theorem

(hf : StrictAnti f) {a} (hmin : ∀ p, f a ≤ p) (x : α) : x ≤ a

Full source

theorem StrictAnti.maximal_of_minimal_image (hf : StrictAnti f) {a} (hmin : ∀ p, f a ≤ p) (x : α) :
    x ≤ a :=
  hf.le_iff_le.mp (hmin (f x))

Maximality of Preimage under Strictly Antitone Function with Minimal Image

Informal description

Let $f : \alpha \to \beta$ be a strictly antitone function between two preorders. If $a \in \alpha$ is such that $f(a)$ is a minimal element in $\beta$ (i.e., $f(a) \leq p$ for all $p \in \beta$), then $a$ is a maximal element in $\alpha$ (i.e., $x \leq a$ for all $x \in \alpha$).

Monotone.strictMono_iff_injective theorem

(hf : Monotone f) : StrictMono f ↔ Injective f

Full source

theorem Monotone.strictMono_iff_injective (hf : Monotone f) : StrictMonoStrictMono f ↔ Injective f :=
  ⟨fun h ↦ h.injective, hf.strictMono_of_injective⟩

Characterization of Strict Monotonicity via Injectivity for Monotone Functions

Informal description

Let $f : \alpha \to \beta$ be a monotone function between preorders. Then $f$ is strictly monotone if and only if it is injective.

Antitone.strictAnti_iff_injective theorem

(hf : Antitone f) : StrictAnti f ↔ Injective f

Full source

theorem Antitone.strictAnti_iff_injective (hf : Antitone f) : StrictAntiStrictAnti f ↔ Injective f :=
  ⟨fun h ↦ h.injective, hf.strictAnti_of_injective⟩

Characterization of Strict Antitonicity via Injectivity for Antitone Functions

Informal description

Let $f : \alpha \to \beta$ be an antitone function between two preorders. Then $f$ is strictly antitone if and only if it is injective.

not_monotone_not_antitone_iff_exists_le_le theorem

 : ¬Monotone f ∧ ¬Antitone f ↔ ∃ a b c, a ≤ b ∧ b ≤ c ∧ ((f a < f b ∧ f c < f b) ∨ (f b < f a ∧ f b < f c))

Full source

/-- A function between linear orders which is neither monotone nor antitone makes a dent upright or
downright. -/
lemma not_monotone_not_antitone_iff_exists_le_le :
    ¬ Monotone f¬ Monotone f ∧ ¬ Antitone f¬ Monotone f ∧ ¬ Antitone f ↔
      ∃ a b c, a ≤ b ∧ b ≤ c ∧ ((f a < f b ∧ f c < f b) ∨ (f b < f a ∧ f b < f c)) := by
  simp_rw [Monotone, Antitone, not_forall, not_le]
  refine Iff.symm ⟨?_, ?_⟩
  · rintro ⟨a, b, c, hab, hbc, ⟨hfab, hfcb⟩ | ⟨hfba, hfbc⟩⟩
    exacts [⟨⟨_, _, hbc, hfcb⟩, _, _, hab, hfab⟩, ⟨⟨_, _, hab, hfba⟩, _, _, hbc, hfbc⟩]
  rintro ⟨⟨a, b, hab, hfba⟩, c, d, hcd, hfcd⟩
  obtain hda | had := le_total d a
  · obtain hfad | hfda := le_total (f a) (f d)
    · exact ⟨c, d, b, hcd, hda.trans hab, Or.inl ⟨hfcd, hfba.trans_le hfad⟩⟩
    · exact ⟨c, a, b, hcd.trans hda, hab, Or.inl ⟨hfcd.trans_le hfda, hfba⟩⟩
  obtain hac | hca := le_total a c
  · obtain hfdb | hfbd := le_or_lt (f d) (f b)
    · exact ⟨a, c, d, hac, hcd, Or.inr ⟨hfcd.trans <| hfdb.trans_lt hfba, hfcd⟩⟩
    obtain hfca | hfac := lt_or_le (f c) (f a)
    · exact ⟨a, c, d, hac, hcd, Or.inr ⟨hfca, hfcd⟩⟩
    obtain hbd | hdb := le_total b d
    · exact ⟨a, b, d, hab, hbd, Or.inr ⟨hfba, hfbd⟩⟩
    · exact ⟨a, d, b, had, hdb, Or.inl ⟨hfac.trans_lt hfcd, hfbd⟩⟩
  · obtain hfdb | hfbd := le_or_lt (f d) (f b)
    · exact ⟨c, a, b, hca, hab, Or.inl ⟨hfcd.trans <| hfdb.trans_lt hfba, hfba⟩⟩
    obtain hfca | hfac := lt_or_le (f c) (f a)
    · exact ⟨c, a, b, hca, hab, Or.inl ⟨hfca, hfba⟩⟩
    obtain hbd | hdb := le_total b d
    · exact ⟨a, b, d, hab, hbd, Or.inr ⟨hfba, hfbd⟩⟩
    · exact ⟨a, d, b, had, hdb, Or.inl ⟨hfac.trans_lt hfcd, hfbd⟩⟩

Characterization of Non-Monotone and Non-Antitone Functions via Weak Local Extrema

Informal description

A function $f : \alpha \to \beta$ between linear orders is neither monotone nor antitone if and only if there exist elements $a, b, c \in \alpha$ with $a \leq b \leq c$ such that either: - $f(a) < f(b)$ and $f(c) < f(b)$, or - $f(b) < f(a)$ and $f(b) < f(c)$.

not_monotone_not_antitone_iff_exists_lt_lt theorem

 : ¬Monotone f ∧ ¬Antitone f ↔ ∃ a b c, a < b ∧ b < c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)

Full source

/-- A function between linear orders which is neither monotone nor antitone makes a dent upright or
downright. -/
lemma not_monotone_not_antitone_iff_exists_lt_lt :
    ¬ Monotone f¬ Monotone f ∧ ¬ Antitone f¬ Monotone f ∧ ¬ Antitone f ↔ ∃ a b c, a < b ∧ b < c ∧
    (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c) := by
  simp_rw [not_monotone_not_antitone_iff_exists_le_le, ← and_assoc]
  refine exists₃_congr (fun a b c ↦ and_congr_left <|
    fun h ↦ (Ne.le_iff_lt ?_).and <| Ne.le_iff_lt ?_) <;>
  (rintro rfl; simp at h)

Characterization of Non-Monotone and Non-Antitone Functions via Local Extrema

Informal description

A function $f : \alpha \to \beta$ between linear orders is neither monotone nor antitone if and only if there exist elements $a, b, c \in \alpha$ with $a < b < c$ such that either: - $f(a) < f(b)$ and $f(c) < f(b)$, or - $f(b) < f(a)$ and $f(b) < f(c)$.

StrictMonoOn.cmp_map_eq theorem

(hf : StrictMonoOn f s) (hx : x ∈ s) (hy : y ∈ s) : cmp (f x) (f y) = cmp x y

Full source

theorem StrictMonoOn.cmp_map_eq (hf : StrictMonoOn f s) (hx : x ∈ s) (hy : y ∈ s) :
    cmp (f x) (f y) = cmp x y :=
  ((hf.compares hx hy).2 (cmp_compares x y)).cmp_eq

Strictly Monotone Function Preserves Comparison on Subset: $\mathrm{cmp}(f(x), f(y)) = \mathrm{cmp}(x, y)$

Informal description

Let $f : \alpha \to \beta$ be a strictly monotone function on a subset $s \subseteq \alpha$ (i.e., for any $x, y \in s$, $x < y$ implies $f(x) < f(y)$). Then for any $x, y \in s$, the comparison of $f(x)$ and $f(y)$ via $\mathrm{cmp}$ is equal to the comparison of $x$ and $y$, i.e., $\mathrm{cmp}(f(x), f(y)) = \mathrm{cmp}(x, y)$.

StrictMono.cmp_map_eq theorem

(hf : StrictMono f) (x y : α) : cmp (f x) (f y) = cmp x y

Full source

theorem StrictMono.cmp_map_eq (hf : StrictMono f) (x y : α) : cmp (f x) (f y) = cmp x y :=
  (hf.strictMonoOn Set.univ).cmp_map_eq trivial trivial

Strictly Monotone Function Preserves Comparison: $\mathrm{cmp}(f(x), f(y)) = \mathrm{cmp}(x, y)$

Informal description

Let $f : \alpha \to \beta$ be a strictly monotone function between two linear orders. Then for any $x, y \in \alpha$, the comparison of $f(x)$ and $f(y)$ via $\mathrm{cmp}$ is equal to the comparison of $x$ and $y$, i.e., $\mathrm{cmp}(f(x), f(y)) = \mathrm{cmp}(x, y)$.

StrictAntiOn.cmp_map_eq theorem

(hf : StrictAntiOn f s) (hx : x ∈ s) (hy : y ∈ s) : cmp (f x) (f y) = cmp y x

Full source

theorem StrictAntiOn.cmp_map_eq (hf : StrictAntiOn f s) (hx : x ∈ s) (hy : y ∈ s) :
    cmp (f x) (f y) = cmp y x :=
  hf.dual_right.cmp_map_eq hy hx

Strictly Antitone Function Reverses Comparison on Subset: $\mathrm{cmp}(f(x), f(y)) = \mathrm{cmp}(y, x)$

Informal description

Let $f : \alpha \to \beta$ be a strictly antitone function on a subset $s \subseteq \alpha$ (i.e., for any $x, y \in s$, $x < y$ implies $f(y) < f(x)$). Then for any $x, y \in s$, the comparison of $f(x)$ and $f(y)$ via $\mathrm{cmp}$ is equal to the comparison of $y$ and $x$, i.e., $\mathrm{cmp}(f(x), f(y)) = \mathrm{cmp}(y, x)$.

StrictAnti.cmp_map_eq theorem

(hf : StrictAnti f) (x y : α) : cmp (f x) (f y) = cmp y x

Full source

theorem StrictAnti.cmp_map_eq (hf : StrictAnti f) (x y : α) : cmp (f x) (f y) = cmp y x :=
  (hf.strictAntiOn Set.univ).cmp_map_eq trivial trivial

Strictly Antitone Function Reverses Comparison: $\mathrm{cmp}(f(x), f(y)) = \mathrm{cmp}(y, x)$

Informal description

Let $f : \alpha \to \beta$ be a strictly antitone function between two linear orders. Then for any $x, y \in \alpha$, the comparison of $f(x)$ and $f(y)$ via $\mathrm{cmp}$ is equal to the comparison of $y$ and $x$, i.e., $\mathrm{cmp}(f(x), f(y)) = \mathrm{cmp}(y, x)$.

Nat.rel_of_forall_rel_succ_of_le_of_lt theorem

 (r : β → β → Prop) [IsTrans β r] {f : ℕ → β} {a : ℕ} (h : ∀ n, a ≤ n → r (f n) (f (n + 1))) ⦃b c : ℕ⦄ (hab : a ≤ b)
  (hbc : b < c) : r (f b) (f c)

Full source

theorem Nat.rel_of_forall_rel_succ_of_le_of_lt (r : β → β → Prop) [IsTrans β r] {f : ℕ → β} {a : ℕ}
    (h : ∀ n, a ≤ n → r (f n) (f (n + 1))) ⦃b c : ℕ⦄ (hab : a ≤ b) (hbc : b < c) :
    r (f b) (f c) := by
  induction hbc with
  | refl => exact h _ hab
  | step b_lt_k r_b_k => exact _root_.trans r_b_k (h _ (hab.trans_lt b_lt_k).le)

Transitivity of Function Values via Successor Relation on Natural Numbers

Informal description

Let $r$ be a transitive binary relation on a type $\beta$, and let $f : \mathbb{N} \to \beta$ be a function. Suppose there exists a natural number $a$ such that for all $n \geq a$, the relation $r(f(n), f(n+1))$ holds. Then for any natural numbers $b$ and $c$ with $a \leq b$ and $b < c$, the relation $r(f(b), f(c))$ holds.

Nat.rel_of_forall_rel_succ_of_le_of_le theorem

 (r : β → β → Prop) [IsRefl β r] [IsTrans β r] {f : ℕ → β} {a : ℕ} (h : ∀ n, a ≤ n → r (f n) (f (n + 1))) ⦃b c : ℕ⦄
  (hab : a ≤ b) (hbc : b ≤ c) : r (f b) (f c)

Full source

theorem Nat.rel_of_forall_rel_succ_of_le_of_le (r : β → β → Prop) [IsRefl β r] [IsTrans β r]
    {f : ℕ → β} {a : ℕ} (h : ∀ n, a ≤ n → r (f n) (f (n + 1)))
    ⦃b c : ℕ⦄ (hab : a ≤ b) (hbc : b ≤ c) : r (f b) (f c) :=
  hbc.eq_or_lt.elim (fun h ↦ h ▸ refl _) (Nat.rel_of_forall_rel_succ_of_le_of_lt r h hab)

Transitive Propagation of Successor Relation on Natural Numbers

Informal description

Let $r$ be a reflexive and transitive binary relation on a type $\beta$, and let $f : \mathbb{N} \to \beta$ be a function. Suppose there exists a natural number $a$ such that for all $n \geq a$, the relation $r(f(n), f(n+1))$ holds. Then for any natural numbers $b$ and $c$ with $a \leq b \leq c$, the relation $r(f(b), f(c))$ holds.

Nat.rel_of_forall_rel_succ_of_lt theorem

 (r : β → β → Prop) [IsTrans β r] {f : ℕ → β} (h : ∀ n, r (f n) (f (n + 1))) ⦃a b : ℕ⦄ (hab : a < b) : r (f a) (f b)

Full source

theorem Nat.rel_of_forall_rel_succ_of_lt (r : β → β → Prop) [IsTrans β r] {f : ℕ → β}
    (h : ∀ n, r (f n) (f (n + 1))) ⦃a b : ℕ⦄ (hab : a < b) : r (f a) (f b) :=
  Nat.rel_of_forall_rel_succ_of_le_of_lt r (fun n _ ↦ h n) le_rfl hab

Transitive Propagation of Successor Relation for Strictly Increasing Natural Numbers

Informal description

Let $r$ be a transitive binary relation on a type $\beta$, and let $f : \mathbb{N} \to \beta$ be a function such that $r(f(n), f(n+1))$ holds for all natural numbers $n$. Then for any natural numbers $a$ and $b$ with $a < b$, the relation $r(f(a), f(b))$ holds.

Nat.rel_of_forall_rel_succ_of_le theorem

 (r : β → β → Prop) [IsRefl β r] [IsTrans β r] {f : ℕ → β} (h : ∀ n, r (f n) (f (n + 1))) ⦃a b : ℕ⦄ (hab : a ≤ b) :
  r (f a) (f b)

Full source

theorem Nat.rel_of_forall_rel_succ_of_le (r : β → β → Prop) [IsRefl β r] [IsTrans β r] {f : ℕ → β}
    (h : ∀ n, r (f n) (f (n + 1))) ⦃a b : ℕ⦄ (hab : a ≤ b) : r (f a) (f b) :=
  Nat.rel_of_forall_rel_succ_of_le_of_le r (fun n _ ↦ h n) le_rfl hab

Propagation of Successor Relation in Natural Numbers via Reflexive-Transitive Closure

Informal description

Let $r$ be a reflexive and transitive binary relation on a type $\beta$, and let $f : \mathbb{N} \to \beta$ be a function such that for every natural number $n$, the relation $r(f(n), f(n+1))$ holds. Then for any natural numbers $a$ and $b$ with $a \leq b$, the relation $r(f(a), f(b))$ holds.

monotone_nat_of_le_succ theorem

{f : ℕ → α} (hf : ∀ n, f n ≤ f (n + 1)) : Monotone f

Full source

theorem monotone_nat_of_le_succ {f : ℕ → α} (hf : ∀ n, f n ≤ f (n + 1)) : Monotone f :=
  Nat.rel_of_forall_rel_succ_of_le (· ≤ ·) hf

Monotonicity of functions on natural numbers with non-decreasing successors

Informal description

Let $f : \mathbb{N} \to \alpha$ be a function such that for every natural number $n$, $f(n) \leq f(n+1)$. Then $f$ is monotone, i.e., for any $a, b \in \mathbb{N}$ with $a \leq b$, we have $f(a) \leq f(b)$.

antitone_nat_of_succ_le theorem

{f : ℕ → α} (hf : ∀ n, f (n + 1) ≤ f n) : Antitone f

Full source

theorem antitone_nat_of_succ_le {f : ℕ → α} (hf : ∀ n, f (n + 1) ≤ f n) : Antitone f :=
  @monotone_nat_of_le_succ αᵒᵈ _ _ hf

Antitonicity of functions on natural numbers with non-increasing successors

Informal description

Let $f : \mathbb{N} \to \alpha$ be a function between preorders such that for every natural number $n$, $f(n+1) \leq f(n)$. Then $f$ is antitone, i.e., for any $m, n \in \mathbb{N}$ with $m \leq n$, we have $f(n) \leq f(m)$.

strictMono_nat_of_lt_succ theorem

{f : ℕ → α} (hf : ∀ n, f n < f (n + 1)) : StrictMono f

Full source

theorem strictMono_nat_of_lt_succ {f : ℕ → α} (hf : ∀ n, f n < f (n + 1)) : StrictMono f :=
  Nat.rel_of_forall_rel_succ_of_lt (· < ·) hf

Strictly increasing function on natural numbers implies strict monotonicity

Informal description

Let $f : \mathbb{N} \to \alpha$ be a function such that for every natural number $n$, we have $f(n) < f(n+1)$. Then $f$ is strictly monotone (i.e., for any $m, n \in \mathbb{N}$, if $m < n$ then $f(m) < f(n)$).

strictAnti_nat_of_succ_lt theorem

{f : ℕ → α} (hf : ∀ n, f (n + 1) < f n) : StrictAnti f

Full source

theorem strictAnti_nat_of_succ_lt {f : ℕ → α} (hf : ∀ n, f (n + 1) < f n) : StrictAnti f :=
  @strictMono_nat_of_lt_succ αᵒᵈ _ f hf

Strictly decreasing function on natural numbers implies strict antitonicity

Informal description

Let $f : \mathbb{N} \to \alpha$ be a function from the natural numbers to a preorder $\alpha$. If for every natural number $n$, the inequality $f(n+1) < f(n)$ holds, then $f$ is strictly antitone (i.e., for any $m, n \in \mathbb{N}$, if $m < n$ then $f(n) < f(m)$).

Nat.exists_strictMono' theorem

[NoMaxOrder α] (a : α) : ∃ f : ℕ → α, StrictMono f ∧ f 0 = a

Full source

/-- If `α` is a preorder with no maximal elements, then there exists a strictly monotone function
`ℕ → α` with any prescribed value of `f 0`. -/
theorem exists_strictMono' [NoMaxOrder α] (a : α) : ∃ f : ℕ → α, StrictMono f ∧ f 0 = a := by
  choose g hg using fun x : α ↦ exists_gt x
  exact ⟨fun n ↦ Nat.recOn n a fun _ ↦ g, strictMono_nat_of_lt_succ fun n ↦ hg _, rfl⟩

Existence of Strictly Increasing Sequence from Any Element in NoMaxOrder

Informal description

Let $\alpha$ be a preorder with no maximal elements. For any element $a \in \alpha$, there exists a strictly increasing function $f \colon \mathbb{N} \to \alpha$ such that $f(0) = a$.

Nat.exists_strictAnti' theorem

[NoMinOrder α] (a : α) : ∃ f : ℕ → α, StrictAnti f ∧ f 0 = a

Full source

/-- If `α` is a preorder with no maximal elements, then there exists a strictly antitone function
`ℕ → α` with any prescribed value of `f 0`. -/
theorem exists_strictAnti' [NoMinOrder α] (a : α) : ∃ f : ℕ → α, StrictAnti f ∧ f 0 = a :=
  exists_strictMono' (OrderDual.toDual a)

Existence of Strictly Decreasing Sequence from Any Element in NoMinOrder

Informal description

Let $\alpha$ be a preorder with no minimal elements. For any element $a \in \alpha$, there exists a strictly decreasing function $f \colon \mathbb{N} \to \alpha$ such that $f(0) = a$.

Nat.exists_strictMono_subsequence theorem

{P : ℕ → Prop} (h : ∀ N, ∃ n > N, P n) : ∃ φ : ℕ → ℕ, StrictMono φ ∧ ∀ n, P (φ n)

Full source

theorem exists_strictMono_subsequence {P : ℕ → Prop} (h : ∀ N, ∃ n > N, P n) :
    ∃ φ : ℕ → ℕ, StrictMono φ ∧ ∀ n, P (φ n) := by
  have : NoMaxOrder {n // P n} :=
    ⟨fun n ↦ Exists.intro ⟨(h n.1).choose, (h n.1).choose_spec.2⟩ (h n.1).choose_spec.1⟩
  obtain ⟨f, hf, _⟩ := Nat.exists_strictMono' (⟨(h 0).choose, (h 0).choose_spec.2⟩ : {n // P n})
  exact Exists.intro (fun n ↦ (f n).1) ⟨hf, fun n ↦ (f n).2⟩

Existence of Strictly Increasing Subsequence Satisfying Predicate in Natural Numbers

Informal description

For any predicate $P$ on natural numbers such that for every natural number $N$ there exists $n > N$ with $P(n)$, there exists a strictly increasing function $\varphi \colon \mathbb{N} \to \mathbb{N}$ such that $P(\varphi(n))$ holds for all $n$.

Nat.exists_strictMono theorem

[Nonempty α] [NoMaxOrder α] : ∃ f : ℕ → α, StrictMono f

Full source

/-- If `α` is a nonempty preorder with no maximal elements, then there exists a strictly monotone
function `ℕ → α`. -/
theorem exists_strictMono [Nonempty α] [NoMaxOrder α] : ∃ f : ℕ → α, StrictMono f :=
  let ⟨a⟩ := ‹Nonempty α›
  let ⟨f, hf, _⟩ := exists_strictMono' a
  ⟨f, hf⟩

Existence of Strictly Increasing Sequence in NoMaxOrder Preorder

Informal description

If $\alpha$ is a nonempty preorder with no maximal elements, then there exists a strictly increasing function $f \colon \mathbb{N} \to \alpha$.

Nat.exists_strictAnti theorem

[Nonempty α] [NoMinOrder α] : ∃ f : ℕ → α, StrictAnti f

Full source

/-- If `α` is a nonempty preorder with no minimal elements, then there exists a strictly antitone
function `ℕ → α`. -/
theorem exists_strictAnti [Nonempty α] [NoMinOrder α] : ∃ f : ℕ → α, StrictAnti f :=
  exists_strictMono αᵒᵈ

Existence of Strictly Decreasing Sequence in NoMinOrder Preorder

Informal description

If $\alpha$ is a nonempty preorder with no minimal elements, then there exists a strictly decreasing function $f \colon \mathbb{N} \to \alpha$.

Nat.pow_self_mono theorem

: Monotone fun n : ℕ ↦ n ^ n

Full source

lemma pow_self_mono : Monotone fun n : ℕ ↦ n ^ n := by
  refine monotone_nat_of_le_succ fun n ↦ ?_
  rw [Nat.pow_succ]
  exact (Nat.pow_le_pow_left n.le_succ _).trans (Nat.le_mul_of_pos_right _ n.succ_pos)

Monotonicity of $n^n$ on Natural Numbers

Informal description

The function $f(n) = n^n$ is monotone on the natural numbers, i.e., for any $m, n \in \mathbb{N}$ with $m \leq n$, we have $m^m \leq n^n$.

Nat.pow_monotoneOn theorem

: MonotoneOn (fun p : ℕ × ℕ ↦ p.1 ^ p.2) {p | p.1 ≠ 0}

Full source

lemma pow_monotoneOn : MonotoneOn (fun p : ℕℕ × ℕ ↦ p.1 ^ p.2) {p | p.1 ≠ 0} := fun _p _ _q hq hpq ↦
  (Nat.pow_le_pow_left hpq.1 _).trans (Nat.pow_le_pow_right (Nat.pos_iff_ne_zero.2 hq) hpq.2)

Monotonicity of Natural Number Exponentiation on Nonzero Base

Informal description

The function $f(p) = p_1^{p_2}$ is monotone on the set $\{p \in \mathbb{N} \times \mathbb{N} \mid p_1 \neq 0\}$. That is, for any pairs $(a_1, a_2), (b_1, b_2) \in \mathbb{N} \times \mathbb{N}$ with $a_1 \neq 0$ and $b_1 \neq 0$, if $(a_1, a_2) \leq (b_1, b_2)$ in the product order, then $a_1^{a_2} \leq b_1^{b_2}$.

Nat.pow_self_strictMonoOn theorem

: StrictMonoOn (fun n : ℕ ↦ n ^ n) {n : ℕ | n ≠ 0}

Full source

lemma pow_self_strictMonoOn : StrictMonoOn (fun n : ℕ ↦ n ^ n) {n : ℕ | n ≠ 0} :=
  fun _m hm _n hn hmn ↦
    (Nat.pow_lt_pow_left hmn hm).trans_le (Nat.pow_le_pow_right (Nat.pos_iff_ne_zero.2 hn) hmn.le)

Strict Monotonicity of $n^n$ on Nonzero Natural Numbers

Informal description

The function $f(n) = n^n$ is strictly increasing on the set of natural numbers $\{n \in \mathbb{N} \mid n \neq 0\}$. That is, for any $m, n \in \mathbb{N}$ with $m < n$ and $m, n \neq 0$, we have $m^m < n^n$.

Int.rel_of_forall_rel_succ_of_lt theorem

 (r : β → β → Prop) [IsTrans β r] {f : ℤ → β} (h : ∀ n, r (f n) (f (n + 1))) ⦃a b : ℤ⦄ (hab : a < b) : r (f a) (f b)

Full source

theorem Int.rel_of_forall_rel_succ_of_lt (r : β → β → Prop) [IsTrans β r] {f : ℤ → β}
    (h : ∀ n, r (f n) (f (n + 1))) ⦃a b : ℤ⦄ (hab : a < b) : r (f a) (f b) := by
  rcases lt.dest hab with ⟨n, rfl⟩
  clear hab
  induction n with
  | zero => rw [Int.ofNat_one]; apply h
  | succ n ihn => rw [Int.natCast_succ, ← Int.add_assoc]; exact _root_.trans ihn (h _)

Transitive Propagation of Successor Relation on Integers

Informal description

Let $\beta$ be a type equipped with a transitive binary relation $r$, and let $f : \mathbb{Z} \to \beta$ be a function such that for every integer $n$, the relation $r(f(n), f(n+1))$ holds. Then for any integers $a < b$, the relation $r(f(a), f(b))$ holds.

Int.rel_of_forall_rel_succ_of_le theorem

 (r : β → β → Prop) [IsRefl β r] [IsTrans β r] {f : ℤ → β} (h : ∀ n, r (f n) (f (n + 1))) ⦃a b : ℤ⦄ (hab : a ≤ b) :
  r (f a) (f b)

Full source

theorem Int.rel_of_forall_rel_succ_of_le (r : β → β → Prop) [IsRefl β r] [IsTrans β r] {f : ℤ → β}
    (h : ∀ n, r (f n) (f (n + 1))) ⦃a b : ℤ⦄ (hab : a ≤ b) : r (f a) (f b) :=
  hab.eq_or_lt.elim (fun h ↦ h ▸ refl _) fun h' ↦ Int.rel_of_forall_rel_succ_of_lt r h h'

Propagation of Successor Relation on Integers for Non-Strict Inequalities

Informal description

Let $\beta$ be a type equipped with a reflexive and transitive binary relation $r$, and let $f : \mathbb{Z} \to \beta$ be a function such that for every integer $n$, the relation $r(f(n), f(n+1))$ holds. Then for any integers $a \leq b$, the relation $r(f(a), f(b))$ holds.

monotone_int_of_le_succ theorem

{f : ℤ → α} (hf : ∀ n, f n ≤ f (n + 1)) : Monotone f

Full source

theorem monotone_int_of_le_succ {f : ℤ → α} (hf : ∀ n, f n ≤ f (n + 1)) : Monotone f :=
  Int.rel_of_forall_rel_succ_of_le (· ≤ ·) hf

Monotonicity Criterion for Integer Functions via Successor Inequality

Informal description

Let $f : \mathbb{Z} \to \alpha$ be a function from the integers to a preorder $\alpha$. If for every integer $n$, we have $f(n) \leq f(n + 1)$, then $f$ is monotone, i.e., for any integers $a \leq b$, we have $f(a) \leq f(b)$.

antitone_int_of_succ_le theorem

{f : ℤ → α} (hf : ∀ n, f (n + 1) ≤ f n) : Antitone f

Full source

theorem antitone_int_of_succ_le {f : ℤ → α} (hf : ∀ n, f (n + 1) ≤ f n) : Antitone f :=
  Int.rel_of_forall_rel_succ_of_le (· ≥ ·) hf

Antitonicity Criterion for Integer Functions via Successor Inequality

Informal description

Let $\alpha$ be a preorder and $f : \mathbb{Z} \to \alpha$ be a function such that for every integer $n$, $f(n+1) \leq f(n)$. Then $f$ is antitone, meaning that for any integers $a \leq b$, we have $f(b) \leq f(a)$.

strictMono_int_of_lt_succ theorem

{f : ℤ → α} (hf : ∀ n, f n < f (n + 1)) : StrictMono f

Full source

theorem strictMono_int_of_lt_succ {f : ℤ → α} (hf : ∀ n, f n < f (n + 1)) : StrictMono f :=
  Int.rel_of_forall_rel_succ_of_lt (· < ·) hf

Strict Monotonicity Criterion for Integer Functions via Successor Inequality

Informal description

Let $f : \mathbb{Z} \to \alpha$ be a function between preorders such that for every integer $n$, $f(n) < f(n+1)$. Then $f$ is strictly monotone, meaning that for any integers $a < b$, we have $f(a) < f(b)$.

strictAnti_int_of_succ_lt theorem

{f : ℤ → α} (hf : ∀ n, f (n + 1) < f n) : StrictAnti f

Full source

theorem strictAnti_int_of_succ_lt {f : ℤ → α} (hf : ∀ n, f (n + 1) < f n) : StrictAnti f :=
  Int.rel_of_forall_rel_succ_of_lt (· > ·) hf

Strict Antitonicity Criterion for Integer Functions via Successor Inequality

Informal description

Let $\alpha$ be a preorder and $f : \mathbb{Z} \to \alpha$ be a function such that for every integer $n$, $f(n+1) < f(n)$. Then $f$ is strictly antitone, meaning that for any integers $a < b$, we have $f(b) < f(a)$.

Int.exists_strictMono theorem

: ∃ f : ℤ → α, StrictMono f

Full source

/-- If `α` is a nonempty preorder with no minimal or maximal elements, then there exists a strictly
monotone function `f : ℤ → α`. -/
theorem exists_strictMono : ∃ f : ℤ → α, StrictMono f := by
  inhabit α
  rcases Nat.exists_strictMono' (default : α) with ⟨f, hf, hf₀⟩
  rcases Nat.exists_strictAnti' (default : α) with ⟨g, hg, hg₀⟩
  refine ⟨fun n ↦ Int.casesOn n f fun n ↦ g (n + 1), strictMono_int_of_lt_succ ?_⟩
  rintro (n | _ | n)
  · exact hf n.lt_succ_self
  · show g 1 < f 0
    rw [hf₀, ← hg₀]
    exact hg Nat.zero_lt_one
  · exact hg (Nat.lt_succ_self _)

Existence of Strictly Monotone Function from Integers to Unbounded Preorder

Informal description

If $\alpha$ is a nonempty preorder with no minimal or maximal elements, then there exists a strictly monotone function $f \colon \mathbb{Z} \to \alpha$.

Int.exists_strictAnti theorem

: ∃ f : ℤ → α, StrictAnti f

Full source

/-- If `α` is a nonempty preorder with no minimal or maximal elements, then there exists a strictly
antitone function `f : ℤ → α`. -/
theorem exists_strictAnti : ∃ f : ℤ → α, StrictAnti f :=
  exists_strictMono αᵒᵈ

Existence of Strictly Antitone Function from Integers to Unbounded Preorder

Informal description

If $\alpha$ is a nonempty preorder with no minimal or maximal elements, then there exists a strictly antitone function $f \colon \mathbb{Z} \to \alpha$, meaning that for all integers $a < b$, we have $f(b) < f(a)$.

Monotone.ne_of_lt_of_lt_nat theorem

{f : ℕ → α} (hf : Monotone f) (n : ℕ) {x : α} (h1 : f n < x) (h2 : x < f (n + 1)) (a : ℕ) : f a ≠ x

Full source

/-- If `f` is a monotone function from `ℕ` to a preorder such that `x` lies between `f n` and
  `f (n + 1)`, then `x` doesn't lie in the range of `f`. -/
theorem Monotone.ne_of_lt_of_lt_nat {f : ℕ → α} (hf : Monotone f) (n : ℕ) {x : α} (h1 : f n < x)
    (h2 : x < f (n + 1)) (a : ℕ) : f a ≠ x := by
  rintro rfl
  exact (hf.reflect_lt h1).not_le (Nat.le_of_lt_succ <| hf.reflect_lt h2)

Monotone Function Gap Property for Natural Numbers

Informal description

Let $f : \mathbb{N} \to \alpha$ be a monotone function from the natural numbers to a preorder $\alpha$. If for some $n \in \mathbb{N}$ and $x \in \alpha$, we have $f(n) < x < f(n+1)$, then $x$ is not in the range of $f$, i.e., $f(a) \neq x$ for any $a \in \mathbb{N}$.

Antitone.ne_of_lt_of_lt_nat theorem

{f : ℕ → α} (hf : Antitone f) (n : ℕ) {x : α} (h1 : f (n + 1) < x) (h2 : x < f n) (a : ℕ) : f a ≠ x

Full source

/-- If `f` is an antitone function from `ℕ` to a preorder such that `x` lies between `f (n + 1)` and
`f n`, then `x` doesn't lie in the range of `f`. -/
theorem Antitone.ne_of_lt_of_lt_nat {f : ℕ → α} (hf : Antitone f) (n : ℕ) {x : α}
    (h1 : f (n + 1) < x) (h2 : x < f n) (a : ℕ) : f a ≠ x := by
  rintro rfl
  exact (hf.reflect_lt h2).not_le (Nat.le_of_lt_succ <| hf.reflect_lt h1)

Antitone Function on Naturals Excludes Intermediate Values

Informal description

Let $f : \mathbb{N} \to \alpha$ be an antitone function from the natural numbers to a preorder $\alpha$. If for some $n \in \mathbb{N}$ and $x \in \alpha$ we have $f(n+1) < x < f(n)$, then $x$ is not in the range of $f$, i.e., $f(a) \neq x$ for any $a \in \mathbb{N}$.

Monotone.ne_of_lt_of_lt_int theorem

{f : ℤ → α} (hf : Monotone f) (n : ℤ) {x : α} (h1 : f n < x) (h2 : x < f (n + 1)) (a : ℤ) : f a ≠ x

Full source

/-- If `f` is a monotone function from `ℤ` to a preorder and `x` lies between `f n` and
  `f (n + 1)`, then `x` doesn't lie in the range of `f`. -/
theorem Monotone.ne_of_lt_of_lt_int {f : ℤ → α} (hf : Monotone f) (n : ℤ) {x : α} (h1 : f n < x)
    (h2 : x < f (n + 1)) (a : ℤ) : f a ≠ x := by
  rintro rfl
  exact (hf.reflect_lt h1).not_le (Int.le_of_lt_add_one <| hf.reflect_lt h2)

Monotone Integer Functions Miss Intermediate Values

Informal description

Let $f : \mathbb{Z} \to \alpha$ be a monotone function from the integers to a preorder $\alpha$. For any integer $n$ and any element $x \in \alpha$ such that $f(n) < x < f(n+1)$, the value $x$ is not in the range of $f$, i.e., $f(a) \neq x$ for all $a \in \mathbb{Z}$.

Antitone.ne_of_lt_of_lt_int theorem

{f : ℤ → α} (hf : Antitone f) (n : ℤ) {x : α} (h1 : f (n + 1) < x) (h2 : x < f n) (a : ℤ) : f a ≠ x

Full source

/-- If `f` is an antitone function from `ℤ` to a preorder and `x` lies between `f (n + 1)` and
`f n`, then `x` doesn't lie in the range of `f`. -/
theorem Antitone.ne_of_lt_of_lt_int {f : ℤ → α} (hf : Antitone f) (n : ℤ) {x : α}
    (h1 : f (n + 1) < x) (h2 : x < f n) (a : ℤ) : f a ≠ x := by
  rintro rfl
  exact (hf.reflect_lt h2).not_le (Int.le_of_lt_add_one <| hf.reflect_lt h1)

Antitone Integer Functions Miss Intermediate Values: $f(n+1) < x < f(n) \Rightarrow x \notin \text{range}(f)$

Informal description

Let $f : \mathbb{Z} \to \alpha$ be an antitone function between preorders, and let $x \in \alpha$. If $x$ satisfies $f(n+1) < x < f(n)$ for some integer $n$, then $x$ is not in the range of $f$, i.e., there exists no integer $a$ such that $f(a) = x$.

Nat.stabilises_of_monotone theorem

 {f : ℕ → ℕ} {b n : ℕ} (hfmono : Monotone f) (hfb : ∀ m, f m ≤ b)
  (hfstab : ∀ m, f m = f (m + 1) → f (m + 1) = f (m + 2)) (hbn : b ≤ n) : f n = f b

Full source

/-- A monotone function `f : ℕ → ℕ` bounded by `b`, which is constant after stabilising for the
first time, stabilises in at most `b` steps. -/
lemma Nat.stabilises_of_monotone {f : ℕ → ℕ} {b n : ℕ} (hfmono : Monotone f) (hfb : ∀ m, f m ≤ b)
    (hfstab : ∀ m, f m = f (m + 1) → f (m + 1) = f (m + 2)) (hbn : b ≤ n) : f n = f b := by
  obtain ⟨m, hmb, hm⟩ : ∃ m ≤ b, f m = f (m + 1) := by
    contrapose! hfb
    let rec strictMono : ∀ m ≤ b + 1, m ≤ f m
    | 0, _ => Nat.zero_le _
    | m + 1, hmb => (strictMono _ <| m.le_succ.trans hmb).trans_lt <| (hfmono m.le_succ).lt_of_ne <|
        hfb _ <| Nat.le_of_succ_le_succ hmb
    exact ⟨b + 1, strictMono _ le_rfl⟩
  replace key : ∀ k : ℕ, f (m + k) = f (m + k + 1) ∧ f (m + k) = f m := fun k =>
    Nat.rec ⟨hm, rfl⟩ (fun k ih => ⟨hfstab _ ih.1, ih.1.symm.trans ih.2⟩) k
  replace key : ∀ k ≥ m, f k = f m := fun k hk =>
    (congr_arg f (Nat.add_sub_of_le hk)).symm.trans (key (k - m)).2
  exact (key n (hmb.trans hbn)).trans (key b hmb).symm

Stabilization of Bounded Monotone Functions on Natural Numbers

Informal description

Let $f : \mathbb{N} \to \mathbb{N}$ be a monotone function bounded above by $b \in \mathbb{N}$ such that whenever $f$ is constant at $m$ and $m+1$, it remains constant thereafter. Then for any $n \geq b$, the function stabilizes to $f(b)$, i.e., $f(n) = f(b)$.

converges_of_monotone_of_bounded theorem

{f : ℕ → ℕ} (mono_f : Monotone f) {c : ℕ} (hc : ∀ n, f n ≤ c) : ∃ b N, ∀ n ≥ N, f n = b

Full source

/-- A bounded monotone function `ℕ → ℕ` converges. -/
lemma converges_of_monotone_of_bounded {f : ℕ → ℕ} (mono_f : Monotone f)
    {c : ℕ} (hc : ∀ n, f n ≤ c) : ∃ b N, ∀ n ≥ N, f n = b := by
  induction c with
  | zero => use 0, 0, fun n _ ↦ Nat.eq_zero_of_le_zero (hc n)
  | succ c ih =>
    by_cases h : ∀ n, f n ≤ c
    · exact ih h
    · push_neg at h; obtain ⟨N, hN⟩ := h
      replace hN : f N = c + 1 := by specialize hc N; omega
      use c + 1, N; intro n hn
      specialize mono_f hn; specialize hc n; omega

Convergence of Bounded Monotone Sequences in $\mathbb{N}$

Informal description

Let $f : \mathbb{N} \to \mathbb{N}$ be a monotone function. If there exists a natural number $c$ such that $f(n) \leq c$ for all $n \in \mathbb{N}$, then there exists a natural number $b$ and a threshold $N \in \mathbb{N}$ such that for all $n \geq N$, $f(n) = b$.

Mathlib.Order.Monotone.Basic

Main theorems

Implementation notes

TODO

Tags