Mathlib.Order.Interval.Set.Monotone

antitone_Ici theorem

: Antitone (Ici : α → Set α)

Full source

theorem antitone_Ici : Antitone (Ici : α → Set α) := fun _ _ => Ici_subset_Ici.2

Antitonicity of Closed Upper Intervals

Informal description

For any type $\alpha$ with a preorder, the function that maps each element $x \in \alpha$ to the closed upper interval $[x, \infty)$ is antitone. That is, if $x \leq y$ in $\alpha$, then $[y, \infty) \subseteq [x, \infty)$.

monotone_Iic theorem

: Monotone (Iic : α → Set α)

Full source

theorem monotone_Iic : Monotone (Iic : α → Set α) := fun _ _ => Iic_subset_Iic.2

Monotonicity of Lower Sets in Partially Ordered Types

Informal description

For any type $\alpha$ with a partial order, the function that maps each element $x \in \alpha$ to the lower set $\{y \in \alpha \mid y \leq x\}$ is monotone. That is, if $x \leq y$, then $\{z \mid z \leq x\} \subseteq \{z \mid z \leq y\}$.

antitone_Ioi theorem

: Antitone (Ioi : α → Set α)

Full source

theorem antitone_Ioi : Antitone (Ioi : α → Set α) := fun _ _ => Ioi_subset_Ioi

Open Upper Interval Function is Antitone

Informal description

For any type $\alpha$ with a partial order, the function mapping each element $x \in \alpha$ to the open upper interval $\{y \in \alpha \mid x < y\}$ is antitone. That is, if $x \leq y$, then $\{z \mid y < z\} \subseteq \{z \mid x < z\}$.

monotone_Iio theorem

: Monotone (Iio : α → Set α)

Full source

theorem monotone_Iio : Monotone (Iio : α → Set α) := fun _ _ => Iio_subset_Iio

Monotonicity of Strict Left-Interval Function

Informal description

For any type $\alpha$ with a partial order, the function that maps each element $x \in \alpha$ to the set $\{y \in \alpha \mid y < x\}$ is monotone. That is, if $x \leq y$, then $\{z \mid z < x\} \subseteq \{z \mid z < y\}$.

Monotone.Ici theorem

(hf : Monotone f) : Antitone fun x => Ici (f x)

Full source

protected theorem Monotone.Ici (hf : Monotone f) : Antitone fun x => Ici (f x) :=
  antitone_Ici.comp_monotone hf

Monotonicity Implies Antitonicity of Upper Intervals

Informal description

If a function $f$ is monotone, then the function that maps each $x$ to the closed upper interval $[f(x), \infty)$ is antitone. That is, for any $x \leq y$, we have $[f(y), \infty) \subseteq [f(x), \infty)$.

MonotoneOn.Ici theorem

(hf : MonotoneOn f s) : AntitoneOn (fun x => Ici (f x)) s

Full source

protected theorem MonotoneOn.Ici (hf : MonotoneOn f s) : AntitoneOn (fun x => Ici (f x)) s :=
  antitone_Ici.comp_monotoneOn hf

Antitonicity of Upper Intervals under Monotone Functions

Informal description

Let $f$ be a function defined on a set $s$ in a preordered type $\alpha$, and suppose $f$ is monotone on $s$. Then the function $x \mapsto [f(x), \infty)$ is antitone on $s$, meaning that for any $x, y \in s$ with $x \leq y$, we have $[f(y), \infty) \subseteq [f(x), \infty)$.

Antitone.Ici theorem

(hf : Antitone f) : Monotone fun x => Ici (f x)

Full source

protected theorem Antitone.Ici (hf : Antitone f) : Monotone fun x => Ici (f x) :=
  antitone_Ici.comp hf

Monotonicity of Upper Intervals under Antitone Functions

Informal description

For any function $f$ that is antitone (order-reversing), the function $x \mapsto [f(x), \infty)$ is monotone (order-preserving). That is, if $f$ is antitone, then for any $x \leq y$, we have $[f(y), \infty) \subseteq [f(x), \infty)$.

AntitoneOn.Ici theorem

(hf : AntitoneOn f s) : MonotoneOn (fun x => Ici (f x)) s

Full source

protected theorem AntitoneOn.Ici (hf : AntitoneOn f s) : MonotoneOn (fun x => Ici (f x)) s :=
  antitone_Ici.comp_antitoneOn hf

Monotonicity of Upper Intervals under Antitone Functions

Informal description

If a function $f$ is antitone on a set $s$, then the function $x \mapsto [f(x), \infty)$ is monotone on $s$.

Monotone.Iic theorem

(hf : Monotone f) : Monotone fun x => Iic (f x)

Full source

protected theorem Monotone.Iic (hf : Monotone f) : Monotone fun x => Iic (f x) :=
  monotone_Iic.comp hf

Monotonicity of Preimage of Lower Sets under Monotone Functions

Informal description

If $f$ is a monotone function from a type $\alpha$ to a partially ordered type $\beta$, then the function mapping each $x \in \alpha$ to the lower set $\{y \in \beta \mid y \leq f(x)\}$ is also monotone. That is, for any $x_1, x_2 \in \alpha$ with $x_1 \leq x_2$, we have $\{y \mid y \leq f(x_1)\} \subseteq \{y \mid y \leq f(x_2)\}$.

MonotoneOn.Iic theorem

(hf : MonotoneOn f s) : MonotoneOn (fun x => Iic (f x)) s

Full source

protected theorem MonotoneOn.Iic (hf : MonotoneOn f s) : MonotoneOn (fun x => Iic (f x)) s :=
  monotone_Iic.comp_monotoneOn hf

Monotonicity of Lower Sets under Monotone Functions

Informal description

Let $f$ be a function defined on a set $s$ in a partially ordered type $\alpha$, and suppose $f$ is monotone on $s$. Then the function that maps each $x \in s$ to the lower set $\{y \in \alpha \mid y \leq f(x)\}$ is also monotone on $s$. That is, for any $x_1, x_2 \in s$ with $x_1 \leq x_2$, we have $\{y \mid y \leq f(x_1)\} \subseteq \{y \mid y \leq f(x_2)\}$.

Antitone.Iic theorem

(hf : Antitone f) : Antitone fun x => Iic (f x)

Full source

protected theorem Antitone.Iic (hf : Antitone f) : Antitone fun x => Iic (f x) :=
  monotone_Iic.comp_antitone hf

Antitone Image of Lower Sets under Antitone Functions

Informal description

Let $f$ be an antitone function from a partially ordered type $\alpha$ to another partially ordered type. Then the function $x \mapsto \{y \mid y \leq f(x)\}$ is also antitone. That is, if $x_1 \leq x_2$, then $\{y \mid y \leq f(x_2)\} \subseteq \{y \mid y \leq f(x_1)\}$.

AntitoneOn.Iic theorem

(hf : AntitoneOn f s) : AntitoneOn (fun x => Iic (f x)) s

Full source

protected theorem AntitoneOn.Iic (hf : AntitoneOn f s) : AntitoneOn (fun x => Iic (f x)) s :=
  monotone_Iic.comp_antitoneOn hf

Antitone Lower Sets of an Antitone Function

Informal description

Let $f$ be a function defined on a set $s$ in a partially ordered type $\alpha$, and suppose $f$ is antitone on $s$ (i.e., for any $x, y \in s$, if $x \leq y$ then $f(y) \leq f(x)$). Then the function $x \mapsto \{z \in \alpha \mid z \leq f(x)\}$ is also antitone on $s$.

Monotone.Ioi theorem

(hf : Monotone f) : Antitone fun x => Ioi (f x)

Full source

protected theorem Monotone.Ioi (hf : Monotone f) : Antitone fun x => Ioi (f x) :=
  antitone_Ioi.comp_monotone hf

Monotonicity Implies Antitonicity of Open Upper Intervals

Informal description

If a function $f$ is monotone, then the function mapping each element $x$ to the open upper interval $\{y \mid f(x) < y\}$ is antitone. That is, for any $x_1 \leq x_2$, we have $\{y \mid f(x_2) < y\} \subseteq \{y \mid f(x_1) < y\}$.

MonotoneOn.Ioi theorem

(hf : MonotoneOn f s) : AntitoneOn (fun x => Ioi (f x)) s

Full source

protected theorem MonotoneOn.Ioi (hf : MonotoneOn f s) : AntitoneOn (fun x => Ioi (f x)) s :=
  antitone_Ioi.comp_monotoneOn hf

Monotonicity Implies Antitonicity of Open Upper Intervals

Informal description

Let $f$ be a function defined on a set $s$ that is monotone on $s$. Then the function mapping each $x \in s$ to the open upper interval $\{y \mid f(x) < y\}$ is antitone on $s$. That is, for any $x_1, x_2 \in s$, if $x_1 \leq x_2$, then $\{y \mid f(x_2) < y\} \subseteq \{y \mid f(x_1) < y\}$.

Antitone.Ioi theorem

(hf : Antitone f) : Monotone fun x => Ioi (f x)

Full source

protected theorem Antitone.Ioi (hf : Antitone f) : Monotone fun x => Ioi (f x) :=
  antitone_Ioi.comp hf

Monotonicity of Open Upper Interval under Antitone Functions

Informal description

If a function $f$ is antitone, then the function mapping each $x$ to the open upper interval $\{y \mid f(x) < y\}$ is monotone. That is, for any $x \leq y$, we have $\{z \mid f(y) < z\} \subseteq \{z \mid f(x) < z\}$.

AntitoneOn.Ioi theorem

(hf : AntitoneOn f s) : MonotoneOn (fun x => Ioi (f x)) s

Full source

protected theorem AntitoneOn.Ioi (hf : AntitoneOn f s) : MonotoneOn (fun x => Ioi (f x)) s :=
  antitone_Ioi.comp_antitoneOn hf

Monotonicity of Open Upper Intervals under Antitone Functions

Informal description

If a function $f$ is antitone on a set $s$, then the function mapping each $x \in s$ to the open upper interval $\{y \mid f(x) < y\}$ is monotone on $s$.

Monotone.Iio theorem

(hf : Monotone f) : Monotone fun x => Iio (f x)

Full source

protected theorem Monotone.Iio (hf : Monotone f) : Monotone fun x => Iio (f x) :=
  monotone_Iio.comp hf

Monotonicity of Strict Left-Interval under Monotone Function

Informal description

If a function $f$ is monotone, then the function that maps each $x$ to the strict left-interval $\{y \mid y < f(x)\}$ is also monotone. That is, for any $x \leq y$, we have $\{z \mid z < f(x)\} \subseteq \{z \mid z < f(y)\}$.

MonotoneOn.Iio theorem

(hf : MonotoneOn f s) : MonotoneOn (fun x => Iio (f x)) s

Full source

protected theorem MonotoneOn.Iio (hf : MonotoneOn f s) : MonotoneOn (fun x => Iio (f x)) s :=
  monotone_Iio.comp_monotoneOn hf

Monotonicity of Strict Left-Interval Function under Monotone Mapping

Informal description

Let $f$ be a function defined on a set $s$ that is monotone on $s$. Then the function mapping each $x \in s$ to the strict left-interval $\{y \mid y < f(x)\}$ is also monotone on $s$. In other words, for any $x_1, x_2 \in s$, if $x_1 \leq x_2$, then $\{y \mid y < f(x_1)\} \subseteq \{y \mid y < f(x_2)\}$.

Antitone.Iio theorem

(hf : Antitone f) : Antitone fun x => Iio (f x)

Full source

protected theorem Antitone.Iio (hf : Antitone f) : Antitone fun x => Iio (f x) :=
  monotone_Iio.comp_antitone hf

Antitonicity of Strict Left-Interval under Antitone Function

Informal description

If a function $f$ is antitone, then the function that maps each $x$ to the strict left-interval $\{y \mid y < f(x)\}$ is also antitone. That is, for any $x_1 \leq x_2$, we have $\{y \mid y < f(x_2)\} \subseteq \{y \mid y < f(x_1)\}$.

AntitoneOn.Iio theorem

(hf : AntitoneOn f s) : AntitoneOn (fun x => Iio (f x)) s

Full source

protected theorem AntitoneOn.Iio (hf : AntitoneOn f s) : AntitoneOn (fun x => Iio (f x)) s :=
  monotone_Iio.comp_antitoneOn hf

Antitonicity of Strict Left-Interval Function under Antitone Mapping

Informal description

Let $f$ be a function defined on a set $s$ that is antitone on $s$. Then the function mapping each $x \in s$ to the strict left-interval $\{y \mid y < f(x)\}$ is also antitone on $s$. In other words, for any $x_1, x_2 \in s$, if $x_1 \leq x_2$, then $\{y \mid y < f(x_2)\} \subseteq \{y \mid y < f(x_1)\}$.

Monotone.Icc theorem

(hf : Monotone f) (hg : Antitone g) : Antitone fun x => Icc (f x) (g x)

Full source

protected theorem Monotone.Icc (hf : Monotone f) (hg : Antitone g) :
    Antitone fun x => Icc (f x) (g x) :=
  hf.Ici.inter hg.Iic

Antitonicity of Interval Function under Monotone and Antitone Mappings

Informal description

Let $f$ be a monotone function and $g$ be an antitone function from a partially ordered type $\alpha$ to another partially ordered type. Then the function $x \mapsto [f(x), g(x)]$ is antitone. That is, if $x_1 \leq x_2$, then $[f(x_2), g(x_2)] \subseteq [f(x_1), g(x_1)]$.

MonotoneOn.Icc theorem

(hf : MonotoneOn f s) (hg : AntitoneOn g s) : AntitoneOn (fun x => Icc (f x) (g x)) s

Full source

protected theorem MonotoneOn.Icc (hf : MonotoneOn f s) (hg : AntitoneOn g s) :
    AntitoneOn (fun x => Icc (f x) (g x)) s :=
  hf.Ici.inter hg.Iic

Antitonicity of Interval Function under Monotone and Antitone Mappings on a Set

Informal description

Let $f$ and $g$ be functions defined on a set $s$ in a partially ordered type $\alpha$, with $f$ monotone on $s$ and $g$ antitone on $s$. Then the function $x \mapsto [f(x), g(x)]$ is antitone on $s$, meaning that for any $x, y \in s$ with $x \leq y$, we have $[f(y), g(y)] \subseteq [f(x), g(x)]$.

Antitone.Icc theorem

(hf : Antitone f) (hg : Monotone g) : Monotone fun x => Icc (f x) (g x)

Full source

protected theorem Antitone.Icc (hf : Antitone f) (hg : Monotone g) :
    Monotone fun x => Icc (f x) (g x) :=
  hf.Ici.inter hg.Iic

Monotonicity of Closed Intervals under Antitone and Monotone Functions

Informal description

If $f$ is an antitone function and $g$ is a monotone function from a partially ordered type to another, then the function $x \mapsto [f(x), g(x)]$ is monotone. That is, for any $x_1 \leq x_2$, we have $[f(x_1), g(x_1)] \subseteq [f(x_2), g(x_2)]$.

AntitoneOn.Icc theorem

(hf : AntitoneOn f s) (hg : MonotoneOn g s) : MonotoneOn (fun x => Icc (f x) (g x)) s

Full source

protected theorem AntitoneOn.Icc (hf : AntitoneOn f s) (hg : MonotoneOn g s) :
    MonotoneOn (fun x => Icc (f x) (g x)) s :=
  hf.Ici.inter hg.Iic

Monotonicity of Closed Intervals under Antitone and Monotone Functions on a Set

Informal description

Let $f$ and $g$ be functions defined on a set $s$ in a partially ordered type, with $f$ antitone on $s$ and $g$ monotone on $s$. Then the function $x \mapsto [f(x), g(x)]$ is monotone on $s$, meaning that for any $x_1, x_2 \in s$ with $x_1 \leq x_2$, we have $[f(x_1), g(x_1)] \subseteq [f(x_2), g(x_2)]$.

Monotone.Ico theorem

(hf : Monotone f) (hg : Antitone g) : Antitone fun x => Ico (f x) (g x)

Full source

protected theorem Monotone.Ico (hf : Monotone f) (hg : Antitone g) :
    Antitone fun x => Ico (f x) (g x) :=
  hf.Ici.inter hg.Iio

Antitonicity of Half-Open Interval under Monotone and Antitone Functions

Informal description

If a function $f$ is monotone and a function $g$ is antitone, then the function that maps each $x$ to the half-open interval $[f(x), g(x))$ is antitone. That is, for any $x \leq y$, we have $[f(y), g(y)) \subseteq [f(x), g(x))$.

MonotoneOn.Ico theorem

(hf : MonotoneOn f s) (hg : AntitoneOn g s) : AntitoneOn (fun x => Ico (f x) (g x)) s

Full source

protected theorem MonotoneOn.Ico (hf : MonotoneOn f s) (hg : AntitoneOn g s) :
    AntitoneOn (fun x => Ico (f x) (g x)) s :=
  hf.Ici.inter hg.Iio

Antitonicity of Half-Open Interval under Monotone and Antitone Functions on a Set

Informal description

Let $f$ be a function defined on a set $s$ that is monotone on $s$, and let $g$ be a function defined on $s$ that is antitone on $s$. Then the function mapping each $x \in s$ to the half-open interval $[f(x), g(x))$ is antitone on $s$. That is, for any $x_1, x_2 \in s$ with $x_1 \leq x_2$, we have $[f(x_2), g(x_2)) \subseteq [f(x_1), g(x_1))$.

Antitone.Ico theorem

(hf : Antitone f) (hg : Monotone g) : Monotone fun x => Ico (f x) (g x)

Full source

protected theorem Antitone.Ico (hf : Antitone f) (hg : Monotone g) :
    Monotone fun x => Ico (f x) (g x) :=
  hf.Ici.inter hg.Iio

Monotonicity of Half-Open Interval under Antitone and Monotone Functions

Informal description

If a function $f$ is antitone and a function $g$ is monotone, then the function that maps each $x$ to the half-open interval $[f(x), g(x))$ is monotone. That is, for any $x \leq y$, we have $[f(x), g(x)) \subseteq [f(y), g(y))$.

AntitoneOn.Ico theorem

(hf : AntitoneOn f s) (hg : MonotoneOn g s) : MonotoneOn (fun x => Ico (f x) (g x)) s

Full source

protected theorem AntitoneOn.Ico (hf : AntitoneOn f s) (hg : MonotoneOn g s) :
    MonotoneOn (fun x => Ico (f x) (g x)) s :=
  hf.Ici.inter hg.Iio

Monotonicity of Half-Open Interval under Antitone and Monotone Functions on a Set

Informal description

Let $f$ be a function defined on a set $s$ that is antitone on $s$, and let $g$ be a function defined on $s$ that is monotone on $s$. Then the function mapping each $x \in s$ to the half-open interval $[f(x), g(x))$ is monotone on $s$. That is, for any $x_1, x_2 \in s$ with $x_1 \leq x_2$, we have $[f(x_1), g(x_1)) \subseteq [f(x_2), g(x_2))$.

Monotone.Ioc theorem

(hf : Monotone f) (hg : Antitone g) : Antitone fun x => Ioc (f x) (g x)

Full source

protected theorem Monotone.Ioc (hf : Monotone f) (hg : Antitone g) :
    Antitone fun x => Ioc (f x) (g x) :=
  hf.Ioi.inter hg.Iic

Antitonicity of Half-Open Interval under Monotone and Antitone Functions

Informal description

If $f$ is a monotone function and $g$ is an antitone function, then the function mapping each $x$ to the half-open interval $(f(x), g(x)]$ is antitone. That is, for any $x_1 \leq x_2$, we have $(f(x_2), g(x_2)] \subseteq (f(x_1), g(x_1)]$.

MonotoneOn.Ioc theorem

(hf : MonotoneOn f s) (hg : AntitoneOn g s) : AntitoneOn (fun x => Ioc (f x) (g x)) s

Full source

protected theorem MonotoneOn.Ioc (hf : MonotoneOn f s) (hg : AntitoneOn g s) :
    AntitoneOn (fun x => Ioc (f x) (g x)) s :=
  hf.Ioi.inter hg.Iic

Antitonicity of Half-Open Interval under Monotone and Antitone Functions on a Set

Informal description

Let $f$ be a function defined on a set $s$ that is monotone on $s$, and let $g$ be a function defined on $s$ that is antitone on $s$. Then the function mapping each $x \in s$ to the half-open interval $(f(x), g(x)]$ is antitone on $s$. That is, for any $x_1, x_2 \in s$ with $x_1 \leq x_2$, we have $(f(x_2), g(x_2)] \subseteq (f(x_1), g(x_1)]$.

Antitone.Ioc theorem

(hf : Antitone f) (hg : Monotone g) : Monotone fun x => Ioc (f x) (g x)

Full source

protected theorem Antitone.Ioc (hf : Antitone f) (hg : Monotone g) :
    Monotone fun x => Ioc (f x) (g x) :=
  hf.Ioi.inter hg.Iic

Monotonicity of Half-Open Intervals under Antitone and Monotone Functions

Informal description

If $f$ is an antitone function and $g$ is a monotone function, then the function mapping each $x$ to the half-open interval $(f(x), g(x)]$ is monotone. That is, for any $x_1 \leq x_2$, we have $(f(x_1), g(x_1)] \subseteq (f(x_2), g(x_2)]$.

AntitoneOn.Ioc theorem

(hf : AntitoneOn f s) (hg : MonotoneOn g s) : MonotoneOn (fun x => Ioc (f x) (g x)) s

Full source

protected theorem AntitoneOn.Ioc (hf : AntitoneOn f s) (hg : MonotoneOn g s) :
    MonotoneOn (fun x => Ioc (f x) (g x)) s :=
  hf.Ioi.inter hg.Iic

Monotonicity of Half-Open Intervals under Antitone and Monotone Functions

Informal description

Let $f$ be an antitone function and $g$ be a monotone function on a set $s$ in a partially ordered type. Then the function that maps each $x \in s$ to the half-open interval $\{y \mid f(x) < y \leq g(x)\}$ is monotone on $s$. That is, for any $x_1, x_2 \in s$ with $x_1 \leq x_2$, we have $\{y \mid f(x_1) < y \leq g(x_1)\} \subseteq \{y \mid f(x_2) < y \leq g(x_2)\}$.

Monotone.Ioo theorem

(hf : Monotone f) (hg : Antitone g) : Antitone fun x => Ioo (f x) (g x)

Full source

protected theorem Monotone.Ioo (hf : Monotone f) (hg : Antitone g) :
    Antitone fun x => Ioo (f x) (g x) :=
  hf.Ioi.inter hg.Iio

Antitonicity of Open Interval under Monotone and Antitone Functions

Informal description

If a function $f$ is monotone and a function $g$ is antitone, then the function that maps each $x$ to the open interval $\{y \mid f(x) < y < g(x)\}$ is antitone. That is, for any $x_1 \leq x_2$, we have $\{y \mid f(x_2) < y < g(x_2)\} \subseteq \{y \mid f(x_1) < y < g(x_1)\}$.

MonotoneOn.Ioo theorem

(hf : MonotoneOn f s) (hg : AntitoneOn g s) : AntitoneOn (fun x => Ioo (f x) (g x)) s

Full source

protected theorem MonotoneOn.Ioo (hf : MonotoneOn f s) (hg : AntitoneOn g s) :
    AntitoneOn (fun x => Ioo (f x) (g x)) s :=
  hf.Ioi.inter hg.Iio

Antitonicity of Open Intervals under Monotone and Antitone Functions on a Set

Informal description

Let $f$ be a function that is monotone on a set $s$, and let $g$ be a function that is antitone on $s$. Then the function mapping each $x \in s$ to the open interval $\{y \mid f(x) < y < g(x)\}$ is antitone on $s$. That is, for any $x_1, x_2 \in s$ with $x_1 \leq x_2$, we have $\{y \mid f(x_2) < y < g(x_2)\} \subseteq \{y \mid f(x_1) < y < g(x_1)\}$.

Antitone.Ioo theorem

(hf : Antitone f) (hg : Monotone g) : Monotone fun x => Ioo (f x) (g x)

Full source

protected theorem Antitone.Ioo (hf : Antitone f) (hg : Monotone g) :
    Monotone fun x => Ioo (f x) (g x) :=
  hf.Ioi.inter hg.Iio

Monotonicity of Open Interval under Antitone and Monotone Functions

Informal description

If a function $f$ is antitone and a function $g$ is monotone, then the function mapping each $x$ to the open interval $\{y \mid f(x) < y < g(x)\}$ is monotone. That is, for any $x_1 \leq x_2$, we have $\{y \mid f(x_1) < y < g(x_1)\} \subseteq \{y \mid f(x_2) < y < g(x_2)\}$.

AntitoneOn.Ioo theorem

(hf : AntitoneOn f s) (hg : MonotoneOn g s) : MonotoneOn (fun x => Ioo (f x) (g x)) s

Full source

protected theorem AntitoneOn.Ioo (hf : AntitoneOn f s) (hg : MonotoneOn g s) :
    MonotoneOn (fun x => Ioo (f x) (g x)) s :=
  hf.Ioi.inter hg.Iio

Monotonicity of Open Intervals under Antitone and Monotone Functions

Informal description

Let $f$ be a function that is antitone on a set $s$, and let $g$ be a function that is monotone on $s$. Then the function mapping each $x \in s$ to the open interval $\{y \mid f(x) < y < g(x)\}$ is monotone on $s$.

iUnion_Ioo_of_mono_of_isGLB_of_isLUB theorem

 (hf : Antitone f) (hg : Monotone g) (ha : IsGLB (range f) a) (hb : IsLUB (range g) b) : ⋃ x, Ioo (f x) (g x) = Ioo a b

Full source

theorem iUnion_Ioo_of_mono_of_isGLB_of_isLUB (hf : Antitone f) (hg : Monotone g)
    (ha : IsGLB (range f) a) (hb : IsLUB (range g) b) : ⋃ x, Ioo (f x) (g x) = Ioo a b :=
  calc
    ⋃ x, Ioo (f x) (g x) = (⋃ x, Ioi (f x)) ∩ ⋃ x, Iio (g x) :=
      iUnion_inter_of_monotone hf.Ioi hg.Iio
    _ = IoiIoi a ∩ Iio b := congr_arg₂ (· ∩ ·) ha.iUnion_Ioi_eq hb.iUnion_Iio_eq

Union of Monotonic Open Intervals Equals Interval of Bounds

Informal description

Let $f$ be an antitone function and $g$ be a monotone function. If $a$ is the greatest lower bound of the range of $f$ and $b$ is the least upper bound of the range of $g$, then the union of all open intervals $\{y \mid f(x) < y < g(x)\}$ for all $x$ is equal to the open interval $(a, b)$.

strictMonoOn_Iic_of_lt_succ theorem

 [SuccOrder α] [IsSuccArchimedean α] {n : α} (hψ : ∀ m, m < n → ψ m < ψ (succ m)) : StrictMonoOn ψ (Set.Iic n)

Full source

/-- A function `ψ` on a `SuccOrder` is strictly monotone before some `n` if for all `m` such that
`m < n`, we have `ψ m < ψ (succ m)`. -/
theorem strictMonoOn_Iic_of_lt_succ [SuccOrder α] [IsSuccArchimedean α] {n : α}
    (hψ : ∀ m, m < n → ψ m < ψ (succ m)) : StrictMonoOn ψ (Set.Iic n) :=
  strictMonoOn_of_lt_succ ordConnected_Iic fun _a ha' _ ha ↦
    hψ _ <| (succ_le_iff_of_not_isMax ha').1 ha

Strict Monotonicity on Lower Set via Successor Condition

Informal description

Let $\alpha$ be a type equipped with a successor order structure `SuccOrder` and assume it is successor-Archimedean. For any element $n \in \alpha$ and function $\psi : \alpha \to \beta$, if for every $m < n$ we have $\psi(m) < \psi(\text{succ}(m))$, then $\psi$ is strictly monotone on the set $\{x \in \alpha \mid x \leq n\}$.

strictAntiOn_Iic_of_succ_lt theorem

 [SuccOrder α] [IsSuccArchimedean α] {n : α} (hψ : ∀ m, m < n → ψ (succ m) < ψ m) : StrictAntiOn ψ (Set.Iic n)

Full source

theorem strictAntiOn_Iic_of_succ_lt [SuccOrder α] [IsSuccArchimedean α] {n : α}
    (hψ : ∀ m, m < n → ψ (succ m) < ψ m) : StrictAntiOn ψ (Set.Iic n) := fun i hi j hj hij =>
  @strictMonoOn_Iic_of_lt_succ α βᵒᵈ _ _ ψ _ _ n hψ i hi j hj hij

Strict Antitonicity on Lower Set via Successor Condition

Informal description

Let $\alpha$ be a type equipped with a successor order structure `SuccOrder` and assume it is successor-Archimedean. For any element $n \in \alpha$ and function $\psi : \alpha \to \beta$, if for every $m < n$ we have $\psi(\text{succ}(m)) < \psi(m)$, then $\psi$ is strictly antitone on the set $\{x \in \alpha \mid x \leq n\}$.

strictMonoOn_Ici_of_pred_lt theorem

 [PredOrder α] [IsPredArchimedean α] {n : α} (hψ : ∀ m, n < m → ψ (pred m) < ψ m) : StrictMonoOn ψ (Set.Ici n)

Full source

theorem strictMonoOn_Ici_of_pred_lt [PredOrder α] [IsPredArchimedean α] {n : α}
    (hψ : ∀ m, n < m → ψ (pred m) < ψ m) : StrictMonoOn ψ (Set.Ici n) := fun i hi j hj hij =>
  @strictMonoOn_Iic_of_lt_succ αᵒᵈ βᵒᵈ _ _ ψ _ _ n hψ j hj i hi hij

Strict Monotonicity on Upper Set via Predecessor Condition

Informal description

Let $\alpha$ be a type equipped with a predecessor order structure `PredOrder` and assume it is predecessor-Archimedean. For any element $n \in \alpha$ and function $\psi : \alpha \to \beta$, if for every $m > n$ we have $\psi(\text{pred}(m)) < \psi(m)$, then $\psi$ is strictly monotone on the set $\{x \in \alpha \mid x \geq n\}$.

strictAntiOn_Ici_of_lt_pred theorem

 [PredOrder α] [IsPredArchimedean α] {n : α} (hψ : ∀ m, n < m → ψ m < ψ (pred m)) : StrictAntiOn ψ (Set.Ici n)

Full source

theorem strictAntiOn_Ici_of_lt_pred [PredOrder α] [IsPredArchimedean α] {n : α}
    (hψ : ∀ m, n < m → ψ m < ψ (pred m)) : StrictAntiOn ψ (Set.Ici n) := fun i hi j hj hij =>
  @strictAntiOn_Iic_of_succ_lt αᵒᵈ βᵒᵈ _ _ ψ _ _ n hψ j hj i hi hij

Strict Antitonicity on Upper Set via Predecessor Condition

Informal description

Let $\alpha$ be a type equipped with a predecessor order structure `PredOrder` and assume it is predecessor-Archimedean. For any element $n \in \alpha$ and function $\psi : \alpha \to \beta$, if for every $m > n$ we have $\psi(m) < \psi(\text{pred}(m))$, then $\psi$ is strictly antitone on the set $\{x \in \alpha \mid x \geq n\}$.

StrictMonoOn.Iic_id_le theorem

 [SuccOrder α] [IsSuccArchimedean α] [OrderBot α] {n : α} {φ : α → α} (hφ : StrictMonoOn φ (Set.Iic n)) :
  ∀ m ≤ n, m ≤ φ m

Full source

theorem StrictMonoOn.Iic_id_le [SuccOrder α] [IsSuccArchimedean α] [OrderBot α] {n : α} {φ : α → α}
    (hφ : StrictMonoOn φ (Set.Iic n)) : ∀ m ≤ n, m ≤ φ m := by
  revert hφ
  refine
    Succ.rec_bot (fun n => StrictMonoOn φ (Set.Iic n) → ∀ m ≤ n, m ≤ φ m)
      (fun _ _ hm => hm.trans bot_le) ?_ _
  rintro k ih hφ m hm
  by_cases hk : IsMax k
  · rw [succ_eq_iff_isMax.2 hk] at hm
    exact ih (hφ.mono <| Iic_subset_Iic.2 (le_succ _)) _ hm
  obtain rfl | h := le_succ_iff_eq_or_le.1 hm
  · specialize ih (StrictMonoOn.mono hφ fun x hx => le_trans hx (le_succ _)) k le_rfl
    refine le_trans (succ_mono ih) (succ_le_of_lt (hφ (le_succ _) le_rfl ?_))
    rw [lt_succ_iff_eq_or_lt_of_not_isMax hk]
    exact Or.inl rfl
  · exact ih (StrictMonoOn.mono hφ fun x hx => le_trans hx (le_succ _)) _ h

Strictly Monotone Function on Lower Set Dominates Identity Function

Informal description

Let $\alpha$ be a type equipped with a successor order structure `SuccOrder`, assume it is successor-Archimedean, and has a bottom element $\bot$. For any element $n \in \alpha$ and function $\varphi : \alpha \to \alpha$, if $\varphi$ is strictly monotone on the lower set $\{x \in \alpha \mid x \leq n\}$, then for all $m \leq n$, we have $m \leq \varphi(m)$.

StrictMonoOn.Ici_le_id theorem

 [PredOrder α] [IsPredArchimedean α] [OrderTop α] {n : α} {φ : α → α} (hφ : StrictMonoOn φ (Set.Ici n)) :
  ∀ m, n ≤ m → φ m ≤ m

Full source

theorem StrictMonoOn.Ici_le_id [PredOrder α] [IsPredArchimedean α] [OrderTop α] {n : α} {φ : α → α}
    (hφ : StrictMonoOn φ (Set.Ici n)) : ∀ m, n ≤ m → φ m ≤ m :=
  StrictMonoOn.Iic_id_le (α := αᵒᵈ) fun _ hi _ hj hij => hφ hj hi hij

Strictly Monotone Function on Upper Set is Bounded Above by Identity

Informal description

Let $\alpha$ be a type equipped with a predecessor order structure `PredOrder`, assume it is predecessor-Archimedean, and has a top element $\top$. For any element $n \in \alpha$ and function $\varphi : \alpha \to \alpha$, if $\varphi$ is strictly monotone on the upper set $\{x \in \alpha \mid x \geq n\}$, then for all $m \geq n$, we have $\varphi(m) \leq m$.