# mathlib3documentation

data.set.intervals.monotone

# Monotonicity on intervals #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we prove that set.Ici etc are monotone/antitone functions. We also prove some lemmas about functions monotone on intervals in succ_orders.

theorem antitone_Ici {α : Type u_1} [preorder α] :
theorem monotone_Iic {α : Type u_1} [preorder α] :
theorem antitone_Ioi {α : Type u_1} [preorder α] :
theorem monotone_Iio {α : Type u_1} [preorder α] :
@[protected]
theorem monotone.Ici {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f : α β} (hf : monotone f) :
antitone (λ (x : α), set.Ici (f x))
@[protected]
theorem monotone_on.Ici {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f : α β} {s : set α} (hf : s) :
antitone_on (λ (x : α), set.Ici (f x)) s
@[protected]
theorem antitone.Ici {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f : α β} (hf : antitone f) :
monotone (λ (x : α), set.Ici (f x))
@[protected]
theorem antitone_on.Ici {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f : α β} {s : set α} (hf : s) :
monotone_on (λ (x : α), set.Ici (f x)) s
@[protected]
theorem monotone.Iic {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f : α β} (hf : monotone f) :
monotone (λ (x : α), set.Iic (f x))
@[protected]
theorem monotone_on.Iic {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f : α β} {s : set α} (hf : s) :
monotone_on (λ (x : α), set.Iic (f x)) s
@[protected]
theorem antitone.Iic {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f : α β} (hf : antitone f) :
antitone (λ (x : α), set.Iic (f x))
@[protected]
theorem antitone_on.Iic {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f : α β} {s : set α} (hf : s) :
antitone_on (λ (x : α), set.Iic (f x)) s
@[protected]
theorem monotone.Ioi {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f : α β} (hf : monotone f) :
antitone (λ (x : α), set.Ioi (f x))
@[protected]
theorem monotone_on.Ioi {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f : α β} {s : set α} (hf : s) :
antitone_on (λ (x : α), set.Ioi (f x)) s
@[protected]
theorem antitone.Ioi {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f : α β} (hf : antitone f) :
monotone (λ (x : α), set.Ioi (f x))
@[protected]
theorem antitone_on.Ioi {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f : α β} {s : set α} (hf : s) :
monotone_on (λ (x : α), set.Ioi (f x)) s
@[protected]
theorem monotone.Iio {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f : α β} (hf : monotone f) :
monotone (λ (x : α), set.Iio (f x))
@[protected]
theorem monotone_on.Iio {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f : α β} {s : set α} (hf : s) :
monotone_on (λ (x : α), set.Iio (f x)) s
@[protected]
theorem antitone.Iio {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f : α β} (hf : antitone f) :
antitone (λ (x : α), set.Iio (f x))
@[protected]
theorem antitone_on.Iio {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f : α β} {s : set α} (hf : s) :
antitone_on (λ (x : α), set.Iio (f x)) s
@[protected]
theorem monotone.Icc {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f g : α β} (hf : monotone f) (hg : antitone g) :
antitone (λ (x : α), set.Icc (f x) (g x))
@[protected]
theorem monotone_on.Icc {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f g : α β} {s : set α} (hf : s) (hg : s) :
antitone_on (λ (x : α), set.Icc (f x) (g x)) s
@[protected]
theorem antitone.Icc {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f g : α β} (hf : antitone f) (hg : monotone g) :
monotone (λ (x : α), set.Icc (f x) (g x))
@[protected]
theorem antitone_on.Icc {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f g : α β} {s : set α} (hf : s) (hg : s) :
monotone_on (λ (x : α), set.Icc (f x) (g x)) s
@[protected]
theorem monotone.Ico {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f g : α β} (hf : monotone f) (hg : antitone g) :
antitone (λ (x : α), set.Ico (f x) (g x))
@[protected]
theorem monotone_on.Ico {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f g : α β} {s : set α} (hf : s) (hg : s) :
antitone_on (λ (x : α), set.Ico (f x) (g x)) s
@[protected]
theorem antitone.Ico {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f g : α β} (hf : antitone f) (hg : monotone g) :
monotone (λ (x : α), set.Ico (f x) (g x))
@[protected]
theorem antitone_on.Ico {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f g : α β} {s : set α} (hf : s) (hg : s) :
monotone_on (λ (x : α), set.Ico (f x) (g x)) s
@[protected]
theorem monotone.Ioc {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f g : α β} (hf : monotone f) (hg : antitone g) :
antitone (λ (x : α), set.Ioc (f x) (g x))
@[protected]
theorem monotone_on.Ioc {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f g : α β} {s : set α} (hf : s) (hg : s) :
antitone_on (λ (x : α), set.Ioc (f x) (g x)) s
@[protected]
theorem antitone.Ioc {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f g : α β} (hf : antitone f) (hg : monotone g) :
monotone (λ (x : α), set.Ioc (f x) (g x))
@[protected]
theorem antitone_on.Ioc {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f g : α β} {s : set α} (hf : s) (hg : s) :
monotone_on (λ (x : α), set.Ioc (f x) (g x)) s
@[protected]
theorem monotone.Ioo {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f g : α β} (hf : monotone f) (hg : antitone g) :
antitone (λ (x : α), set.Ioo (f x) (g x))
@[protected]
theorem monotone_on.Ioo {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f g : α β} {s : set α} (hf : s) (hg : s) :
antitone_on (λ (x : α), set.Ioo (f x) (g x)) s
@[protected]
theorem antitone.Ioo {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f g : α β} (hf : antitone f) (hg : monotone g) :
monotone (λ (x : α), set.Ioo (f x) (g x))
@[protected]
theorem antitone_on.Ioo {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f g : α β} {s : set α} (hf : s) (hg : s) :
monotone_on (λ (x : α), set.Ioo (f x) (g x)) s
theorem Union_Ioo_of_mono_of_is_glb_of_is_lub {α : Type u_1} {β : Type u_2} [linear_order β] {f g : α β} {a b : β} (hf : antitone f) (hg : monotone g) (ha : is_glb (set.range f) a) (hb : is_lub (set.range g) b) :
( (x : α), set.Ioo (f x) (g x)) = b
theorem strict_mono_on.Iic_id_le {α : Type u_1} [succ_order α] [order_bot α] {n : α} {φ : α α} (hφ : (set.Iic n)) (m : α) (H : m n) :
m φ m
theorem strict_mono_on.Ici_le_id {α : Type u_1} [pred_order α] [order_top α] {n : α} {φ : α α} (hφ : (set.Ici n)) (m : α) :
n m φ m m
theorem strict_mono_on_Iic_of_lt_succ {α : Type u_1} {β : Type u_2} [preorder β] {ψ : α β} [succ_order α] {n : α} (hψ : (m : α), m < n ψ m < ψ (order.succ m)) :
(set.Iic n)

A function ψ on a succ_order is strictly monotone before some n if for all m such that m < n, we have ψ m < ψ (succ m).

theorem strict_anti_on_Iic_of_succ_lt {α : Type u_1} {β : Type u_2} [preorder β] {ψ : α β} [succ_order α] {n : α} (hψ : (m : α), m < n ψ (order.succ m) < ψ m) :
(set.Iic n)
theorem strict_mono_on_Ici_of_pred_lt {α : Type u_1} {β : Type u_2} [preorder β] {ψ : α β} [pred_order α] {n : α} (hψ : (m : α), n < m ψ (order.pred m) < ψ m) :
(set.Ici n)
theorem strict_anti_on_Ici_of_lt_pred {α : Type u_1} {β : Type u_2} [preorder β] {ψ : α β} [pred_order α] {n : α} (hψ : (m : α), n < m ψ m < ψ (order.pred m)) :
(set.Ici n)