mathlib3 documentation

data.set.intervals.surj_on

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