Monotone functions on intervals #
This file shows many variants of the fact that a monotone function f sends an interval with
endpoints a and b to the interval with endpoints f a and f b.
theorem
MonotoneOn.mapsTo_Ici
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[Preorder α]
[Preorder β]
{a : α}
(h : MonotoneOn f (Set.Ici a))
:
Set.MapsTo f (Set.Ici a) (Set.Ici (f a))
theorem
MonotoneOn.mapsTo_Iic
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[Preorder α]
[Preorder β]
{b : α}
(h : MonotoneOn f (Set.Iic b))
:
Set.MapsTo f (Set.Iic b) (Set.Iic (f b))
theorem
MonotoneOn.mapsTo_Icc
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[Preorder α]
[Preorder β]
{a b : α}
(h : MonotoneOn f (Set.Icc a b))
:
Set.MapsTo f (Set.Icc a b) (Set.Icc (f a) (f b))
theorem
AntitoneOn.mapsTo_Ici
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[Preorder α]
[Preorder β]
{a : α}
(h : AntitoneOn f (Set.Ici a))
:
Set.MapsTo f (Set.Ici a) (Set.Iic (f a))
theorem
AntitoneOn.mapsTo_Iic
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[Preorder α]
[Preorder β]
{b : α}
(h : AntitoneOn f (Set.Iic b))
:
Set.MapsTo f (Set.Iic b) (Set.Ici (f b))
theorem
AntitoneOn.mapsTo_Icc
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[Preorder α]
[Preorder β]
{a b : α}
(h : AntitoneOn f (Set.Icc a b))
:
Set.MapsTo f (Set.Icc a b) (Set.Icc (f b) (f a))
theorem
StrictMonoOn.mapsTo_Ioi
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[Preorder α]
[Preorder β]
{a : α}
(h : StrictMonoOn f (Set.Ici a))
:
Set.MapsTo f (Set.Ioi a) (Set.Ioi (f a))
theorem
StrictMonoOn.mapsTo_Iio
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[Preorder α]
[Preorder β]
{b : α}
(h : StrictMonoOn f (Set.Iic b))
:
Set.MapsTo f (Set.Iio b) (Set.Iio (f b))
theorem
StrictMonoOn.mapsTo_Ioo
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[Preorder α]
[Preorder β]
{a b : α}
(h : StrictMonoOn f (Set.Icc a b))
:
Set.MapsTo f (Set.Ioo a b) (Set.Ioo (f a) (f b))
theorem
StrictAntiOn.mapsTo_Ioi
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[Preorder α]
[Preorder β]
{a : α}
(h : StrictAntiOn f (Set.Ici a))
:
Set.MapsTo f (Set.Ioi a) (Set.Iio (f a))
theorem
StrictAntiOn.mapsTo_Iio
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[Preorder α]
[Preorder β]
{b : α}
(h : StrictAntiOn f (Set.Iic b))
:
Set.MapsTo f (Set.Iio b) (Set.Ioi (f b))
theorem
StrictAntiOn.mapsTo_Ioo
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[Preorder α]
[Preorder β]
{a b : α}
(h : StrictAntiOn f (Set.Icc a b))
:
Set.MapsTo f (Set.Ioo a b) (Set.Ioo (f b) (f a))
theorem
Monotone.mapsTo_Ici
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[Preorder α]
[Preorder β]
{a : α}
(h : Monotone f)
:
Set.MapsTo f (Set.Ici a) (Set.Ici (f a))
theorem
Monotone.mapsTo_Iic
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[Preorder α]
[Preorder β]
{b : α}
(h : Monotone f)
:
Set.MapsTo f (Set.Iic b) (Set.Iic (f b))
theorem
Monotone.mapsTo_Icc
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[Preorder α]
[Preorder β]
{a b : α}
(h : Monotone f)
:
Set.MapsTo f (Set.Icc a b) (Set.Icc (f a) (f b))
theorem
Antitone.mapsTo_Ici
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[Preorder α]
[Preorder β]
{a : α}
(h : Antitone f)
:
Set.MapsTo f (Set.Ici a) (Set.Iic (f a))
theorem
Antitone.mapsTo_Iic
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[Preorder α]
[Preorder β]
{b : α}
(h : Antitone f)
:
Set.MapsTo f (Set.Iic b) (Set.Ici (f b))
theorem
Antitone.mapsTo_Icc
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[Preorder α]
[Preorder β]
{a b : α}
(h : Antitone f)
:
Set.MapsTo f (Set.Icc a b) (Set.Icc (f b) (f a))
theorem
StrictMono.mapsTo_Ioi
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[Preorder α]
[Preorder β]
{a : α}
(h : StrictMono f)
:
Set.MapsTo f (Set.Ioi a) (Set.Ioi (f a))
theorem
StrictMono.mapsTo_Iio
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[Preorder α]
[Preorder β]
{b : α}
(h : StrictMono f)
:
Set.MapsTo f (Set.Iio b) (Set.Iio (f b))
theorem
StrictMono.mapsTo_Ioo
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[Preorder α]
[Preorder β]
{a b : α}
(h : StrictMono f)
:
Set.MapsTo f (Set.Ioo a b) (Set.Ioo (f a) (f b))
theorem
StrictAnti.mapsTo_Ioi
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[Preorder α]
[Preorder β]
{a : α}
(h : StrictAnti f)
:
Set.MapsTo f (Set.Ioi a) (Set.Iio (f a))
theorem
StrictAnti.mapsTo_Iio
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[Preorder α]
[Preorder β]
{b : α}
(h : StrictAnti f)
:
Set.MapsTo f (Set.Iio b) (Set.Ioi (f b))
theorem
StrictAnti.mapsTo_Ioo
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[Preorder α]
[Preorder β]
{a b : α}
(h : StrictAnti f)
:
Set.MapsTo f (Set.Ioo a b) (Set.Ioo (f b) (f a))
theorem
StrictMonoOn.mapsTo_Ico
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[PartialOrder α]
[Preorder β]
{a b : α}
(h : StrictMonoOn f (Set.Icc a b))
:
Set.MapsTo f (Set.Ico a b) (Set.Ico (f a) (f b))
theorem
StrictMonoOn.mapsTo_Ioc
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[PartialOrder α]
[Preorder β]
{a b : α}
(h : StrictMonoOn f (Set.Icc a b))
:
Set.MapsTo f (Set.Ioc a b) (Set.Ioc (f a) (f b))
theorem
StrictAntiOn.mapsTo_Ico
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[PartialOrder α]
[Preorder β]
{a b : α}
(h : StrictAntiOn f (Set.Icc a b))
:
Set.MapsTo f (Set.Ico a b) (Set.Ioc (f b) (f a))
theorem
StrictAntiOn.mapsTo_Ioc
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[PartialOrder α]
[Preorder β]
{a b : α}
(h : StrictAntiOn f (Set.Icc a b))
:
Set.MapsTo f (Set.Ioc a b) (Set.Ico (f b) (f a))
theorem
StrictMono.mapsTo_Ico
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[PartialOrder α]
[Preorder β]
{a b : α}
(h : StrictMono f)
:
Set.MapsTo f (Set.Ico a b) (Set.Ico (f a) (f b))
theorem
StrictMono.mapsTo_Ioc
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[PartialOrder α]
[Preorder β]
{a b : α}
(h : StrictMono f)
:
Set.MapsTo f (Set.Ioc a b) (Set.Ioc (f a) (f b))
theorem
StrictAnti.mapsTo_Ico
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[PartialOrder α]
[Preorder β]
{a b : α}
(h : StrictAnti f)
:
Set.MapsTo f (Set.Ico a b) (Set.Ioc (f b) (f a))
theorem
StrictAnti.mapsTo_Ioc
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[PartialOrder α]
[Preorder β]
{a b : α}
(h : StrictAnti f)
:
Set.MapsTo f (Set.Ioc a b) (Set.Ico (f b) (f a))
theorem
StrictMonoOn.image_Ico_subset
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[PartialOrder α]
[Preorder β]
{a b : α}
(h : StrictMonoOn f (Set.Icc a b))
:
theorem
StrictMonoOn.image_Ioc_subset
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[PartialOrder α]
[Preorder β]
{a b : α}
(h : StrictMonoOn f (Set.Icc a b))
:
theorem
StrictAntiOn.image_Ico_subset
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[PartialOrder α]
[Preorder β]
{a b : α}
(h : StrictAntiOn f (Set.Icc a b))
:
theorem
StrictAntiOn.image_Ioc_subset
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[PartialOrder α]
[Preorder β]
{a b : α}
(h : StrictAntiOn f (Set.Icc a b))
:
theorem
StrictMono.image_Ico_subset
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[PartialOrder α]
[Preorder β]
{a b : α}
(h : StrictMono f)
:
theorem
StrictMono.image_Ioc_subset
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[PartialOrder α]
[Preorder β]
{a b : α}
(h : StrictMono f)
:
theorem
StrictAnti.image_Ico_subset
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[PartialOrder α]
[Preorder β]
{a b : α}
(h : StrictAnti f)
:
theorem
StrictAnti.image_Ioc_subset
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[PartialOrder α]
[Preorder β]
{a b : α}
(h : StrictAnti f)
:
theorem
directedOn_le_Iic
{α : Type u_1}
[Preorder α]
(b : α)
:
DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) (Set.Iic b)
theorem
directedOn_le_Icc
{α : Type u_1}
[Preorder α]
(a b : α)
:
DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) (Set.Icc a b)
theorem
directedOn_le_Ioc
{α : Type u_1}
[Preorder α]
(a b : α)
:
DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) (Set.Ioc a b)
theorem
directedOn_ge_Ici
{α : Type u_1}
[Preorder α]
(a : α)
:
DirectedOn (fun (x1 x2 : α) => x1 ≥ x2) (Set.Ici a)
theorem
directedOn_ge_Icc
{α : Type u_1}
[Preorder α]
(a b : α)
:
DirectedOn (fun (x1 x2 : α) => x1 ≥ x2) (Set.Icc a b)
theorem
directedOn_ge_Ico
{α : Type u_1}
[Preorder α]
(a b : α)
:
DirectedOn (fun (x1 x2 : α) => x1 ≥ x2) (Set.Ico a b)