mathlib documentation

data.set.intervals.monotone

Monotonicity on intervals #

In this file we prove that a function is (strictly) monotone (or antitone) on a linear order α provided that it is (strictly) monotone on (-∞, a] and on [a, +∞). We also provide an order isomorphism order_iso_Ioo_neg_one_one between the open interval (-1, 1) in a linear ordered field and the whole field.

@[protected]
theorem strict_mono_on.Iic_union_Ici {α : Type u_1} {β : Type u_2} [linear_order α] [preorder β] {a : α} {f : α → β} (h₁ : strict_mono_on f (set.Iic a)) (h₂ : strict_mono_on f (set.Ici a)) :

If f is strictly monotone both on (-∞, a] and [a, ∞), then it is strictly monotone on the whole line.

@[protected]
theorem strict_anti_on.Iic_union_Ici {α : Type u_1} {β : Type u_2} [linear_order α] [preorder β] {a : α} {f : α → β} (h₁ : strict_anti_on f (set.Iic a)) (h₂ : strict_anti_on f (set.Ici a)) :

If f is strictly antitone both on (-∞, a] and [a, ∞), then it is strictly antitone on the whole line.

@[protected]
theorem monotone_on.Iic_union_Ici {α : Type u_1} {β : Type u_2} [linear_order α] [preorder β] {a : α} {f : α → β} (h₁ : monotone_on f (set.Iic a)) (h₂ : monotone_on f (set.Ici a)) :
@[protected]
theorem antitone_on.Iic_union_Ici {α : Type u_1} {β : Type u_2} [linear_order α] [preorder β] {a : α} {f : α → β} (h₁ : antitone_on f (set.Iic a)) (h₂ : antitone_on f (set.Ici a)) :
theorem strict_mono_of_odd_strict_mono_on_nonneg {G : Type u_1} {H : Type u_2} [linear_ordered_add_comm_group G] [ordered_add_comm_group H] {f : G → H} (h₁ : ∀ (x : G), f (-x) = -f x) (h₂ : strict_mono_on f (set.Ici 0)) :
theorem monotone_of_odd_of_monotone_on_nonneg {G : Type u_1} {H : Type u_2} [linear_ordered_add_comm_group G] [ordered_add_comm_group H] {f : G → H} (h₁ : ∀ (x : G), f (-x) = -f x) (h₂ : monotone_on f (set.Ici 0)) :
@[irreducible]
def order_iso_Ioo_neg_one_one (k : Type u_1) [linear_ordered_field k] :
k ≃o (set.Ioo (-1) 1)

In a linear ordered field, the whole field is order isomorphic to the open interval (-1, 1). We consider the actual implementation to be a "black box", so it is irreducible.

Equations
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)) :