mathlib documentation

data.set.intervals.surj_on

Monotone surjective functions are surjective on intervals

A monotone surjective function sends any interval in the range 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 : α} :
a bset.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 : α) :

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

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

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