Documentation

Mathlib.Data.Set.Intervals.SurjOn

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