mathlib documentation

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 : monotone_on f 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 : antitone_on f 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 : monotone_on f 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 : antitone_on f 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 : monotone_on f 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 : antitone_on f 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 : monotone_on f 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 : antitone_on f 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 : monotone_on f s) (hg : antitone_on g 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 : antitone_on f s) (hg : monotone_on g 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 : monotone_on f s) (hg : antitone_on g 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 : antitone_on f s) (hg : monotone_on g 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 : monotone_on f s) (hg : antitone_on g 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 : antitone_on f s) (hg : monotone_on g 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 : monotone_on f s) (hg : antitone_on g 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 : antitone_on f s) (hg : monotone_on g 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} [semilattice_sup α] [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)) = set.Ioo a b
theorem strict_mono_on.Iic_id_le {α : Type u_1} [partial_order α] [succ_order α] [is_succ_archimedean α] [order_bot α] {n : α} {φ : α α} (hφ : strict_mono_on φ (set.Iic n)) (m : α) (H : m n) :
m φ m
theorem strict_mono_on.Iic_le_id {α : Type u_1} [partial_order α] [pred_order α] [is_pred_archimedean α] [order_top α] {n : α} {φ : α α} (hφ : strict_mono_on φ (set.Ici n)) (m : α) :
n m φ m m
theorem strict_mono_on_Iic_of_lt_succ {α : Type u_1} {β : Type u_2} [partial_order α] [preorder β] {ψ : α β} [succ_order α] [is_succ_archimedean α] {n : α} (hψ : (m : α), m < n ψ m < ψ (order.succ m)) :

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} [partial_order α] [preorder β] {ψ : α β} [succ_order α] [is_succ_archimedean α] {n : α} (hψ : (m : α), m < n ψ (order.succ m) < ψ m) :
theorem strict_mono_on_Iic_of_pred_lt {α : Type u_1} {β : Type u_2} [partial_order α] [preorder β] {ψ : α β} [pred_order α] [is_pred_archimedean α] {n : α} (hψ : (m : α), n < m ψ (order.pred m) < ψ m) :
theorem strict_anti_on_Iic_of_lt_pred {α : Type u_1} {β : Type u_2} [partial_order α] [preorder β] {ψ : α β} [pred_order α] [is_pred_archimedean α] {n : α} (hψ : (m : α), n < m ψ m < ψ (order.pred m)) :