Monotone surjective functions are surjective on intervals #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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.surj_on, and provided for all
permutations of interval endpoints.
theorem
surj_on_Ioo_of_monotone_surjective
{α : Type u_1}
{β : Type u_2}
[linear_order α]
[partial_order β]
{f : α → β}
(h_mono : monotone f)
(h_surj : function.surjective f)
(a b : α) :
set.surj_on f (set.Ioo a b) (set.Ioo (f a) (f b))
theorem
surj_on_Ico_of_monotone_surjective
{α : Type u_1}
{β : Type u_2}
[linear_order α]
[partial_order β]
{f : α → β}
(h_mono : monotone f)
(h_surj : function.surjective f)
(a b : α) :
set.surj_on f (set.Ico a b) (set.Ico (f a) (f b))
theorem
surj_on_Ioc_of_monotone_surjective
{α : Type u_1}
{β : Type u_2}
[linear_order α]
[partial_order β]
{f : α → β}
(h_mono : monotone f)
(h_surj : function.surjective f)
(a b : α) :
set.surj_on f (set.Ioc a b) (set.Ioc (f a) (f b))
theorem
surj_on_Icc_of_monotone_surjective
{α : Type u_1}
{β : Type u_2}
[linear_order α]
[partial_order β]
{f : α → β}
(h_mono : monotone f)
(h_surj : function.surjective f)
{a b : α}
(hab : a ≤ b) :
set.surj_on f (set.Icc a b) (set.Icc (f a) (f b))
theorem
surj_on_Ioi_of_monotone_surjective
{α : Type u_1}
{β : Type u_2}
[linear_order α]
[partial_order β]
{f : α → β}
(h_mono : monotone f)
(h_surj : function.surjective f)
(a : α) :
set.surj_on f (set.Ioi a) (set.Ioi (f a))
theorem
surj_on_Iio_of_monotone_surjective
{α : Type u_1}
{β : Type u_2}
[linear_order α]
[partial_order β]
{f : α → β}
(h_mono : monotone f)
(h_surj : function.surjective f)
(a : α) :
set.surj_on f (set.Iio a) (set.Iio (f a))
theorem
surj_on_Ici_of_monotone_surjective
{α : Type u_1}
{β : Type u_2}
[linear_order α]
[partial_order β]
{f : α → β}
(h_mono : monotone f)
(h_surj : function.surjective f)
(a : α) :
set.surj_on f (set.Ici a) (set.Ici (f a))
theorem
surj_on_Iic_of_monotone_surjective
{α : Type u_1}
{β : Type u_2}
[linear_order α]
[partial_order β]
{f : α → β}
(h_mono : monotone f)
(h_surj : function.surjective f)
(a : α) :
set.surj_on f (set.Iic a) (set.Iic (f a))