Monotone surjective functions are surjective on intervals #
A monotone surjective function sends any interval in the domain onto the interval with corresponding
endpoints in the range. This is expressed in this file using Set.surjOn, and provided for all
permutations of interval endpoints.
theorem
surjOn_Ioo_of_monotone_surjective
{α : Type u_1}
{β : Type u_2}
[LinearOrder α]
[PartialOrder β]
{f : α → β}
(h_mono : Monotone f)
(h_surj : Function.Surjective f)
(a : α)
(b : α)
:
Set.SurjOn f (Set.Ioo a b) (Set.Ioo (f a) (f b))
theorem
surjOn_Ico_of_monotone_surjective
{α : Type u_1}
{β : Type u_2}
[LinearOrder α]
[PartialOrder β]
{f : α → β}
(h_mono : Monotone f)
(h_surj : Function.Surjective f)
(a : α)
(b : α)
:
Set.SurjOn f (Set.Ico a b) (Set.Ico (f a) (f b))
theorem
surjOn_Ioc_of_monotone_surjective
{α : Type u_1}
{β : Type u_2}
[LinearOrder α]
[PartialOrder β]
{f : α → β}
(h_mono : Monotone f)
(h_surj : Function.Surjective f)
(a : α)
(b : α)
:
Set.SurjOn f (Set.Ioc a b) (Set.Ioc (f a) (f b))
theorem
surjOn_Icc_of_monotone_surjective
{α : Type u_1}
{β : Type u_2}
[LinearOrder α]
[PartialOrder β]
{f : α → β}
(h_mono : Monotone f)
(h_surj : Function.Surjective f)
{a : α}
{b : α}
(hab : a ≤ b)
:
Set.SurjOn f (Set.Icc a b) (Set.Icc (f a) (f b))
theorem
surjOn_Ioi_of_monotone_surjective
{α : Type u_1}
{β : Type u_2}
[LinearOrder α]
[PartialOrder β]
{f : α → β}
(h_mono : Monotone f)
(h_surj : Function.Surjective f)
(a : α)
:
Set.SurjOn f (Set.Ioi a) (Set.Ioi (f a))
theorem
surjOn_Iio_of_monotone_surjective
{α : Type u_1}
{β : Type u_2}
[LinearOrder α]
[PartialOrder β]
{f : α → β}
(h_mono : Monotone f)
(h_surj : Function.Surjective f)
(a : α)
:
Set.SurjOn f (Set.Iio a) (Set.Iio (f a))
theorem
surjOn_Ici_of_monotone_surjective
{α : Type u_1}
{β : Type u_2}
[LinearOrder α]
[PartialOrder β]
{f : α → β}
(h_mono : Monotone f)
(h_surj : Function.Surjective f)
(a : α)
:
Set.SurjOn f (Set.Ici a) (Set.Ici (f a))
theorem
surjOn_Iic_of_monotone_surjective
{α : Type u_1}
{β : Type u_2}
[LinearOrder α]
[PartialOrder β]
{f : α → β}
(h_mono : Monotone f)
(h_surj : Function.Surjective f)
(a : α)
:
Set.SurjOn f (Set.Iic a) (Set.Iic (f a))