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.

source
@[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)) :
strict_mono f

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

source
@[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)) :
strict_anti f

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

source
@[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)) :
monotone f
source
@[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)) :
antitone f
source
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)) :
strict_mono f
source
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)) :
monotone f
source
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
source
theorem antitone_Ici {α : Type u_1} [preorder α] :
antitone set.Ici
source
theorem monotone_Iic {α : Type u_1} [preorder α] :
monotone set.Iic
source
theorem antitone_Ioi {α : Type u_1} [preorder α] :
antitone set.Ioi
source
theorem monotone_Iio {α : Type u_1} [preorder α] :
monotone set.Iio
source
@[protected]
theorem monotone.Ici {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f : α → β} (hf : monotone f) :
antitone (λ (x : α), set.Ici (f x))
source
@[protected]
theorem antitone.Ici {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f : α → β} (hf : antitone f) :
monotone (λ (x : α), set.Ici (f x))
source
@[protected]
theorem monotone.Iic {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f : α → β} (hf : monotone f) :
monotone (λ (x : α), set.Iic (f x))
source
@[protected]
theorem antitone.Iic {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f : α → β} (hf : antitone f) :
antitone (λ (x : α), set.Iic (f x))
source
@[protected]
theorem monotone.Ioi {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f : α → β} (hf : monotone f) :
antitone (λ (x : α), set.Ioi (f x))
source
@[protected]
theorem antitone.Ioi {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f : α → β} (hf : antitone f) :
monotone (λ (x : α), set.Ioi (f x))
source
@[protected]
theorem monotone.Iio {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f : α → β} (hf : monotone f) :
monotone (λ (x : α), set.Iio (f x))
source
@[protected]
theorem antitone.Iio {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f : α → β} (hf : antitone f) :
antitone (λ (x : α), set.Iio (f x))
source
@[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))
source
@[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))
source
@[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))
source
@[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))
source
@[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))
source
@[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))
source
@[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))
source
@[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))
source
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