English
Let f be a monotone surjective map between ordered types. Then for all a and b, the image of the half-open interval (a, b] under f covers the half-open interval (f(a), f(b)]. In other words, every y with f(a) < y ≤ f(b) is obtained as f(x) for some x with a < x ≤ b.
Русский
Пусть f монотонна и сюръективна между упорядоченными множествами. Тогда для любых a, b отображение f отображает полуоткрытый интервал (a, b] на интервал (f(a), f(b)], то есть каждый y с f(a) < y ≤ f(b) существует x, такое что a < x ≤ b и f(x) = y.
LaTeX
$$$$\text{SurjOn}(f, Ioc(a,b), Ioc(f(a),f(b))).$$$$
Lean4
theorem surjOn_Ioc_of_monotone_surjective (h_mono : Monotone f) (h_surj : Function.Surjective f) (a b : α) :
SurjOn f (Ioc a b) (Ioc (f a) (f b)) := by
simpa using
surjOn_Ico_of_monotone_surjective h_mono.dual h_surj (toDual b)
(toDual a)
-- to see that the hypothesis `a ≤ b` is necessary, consider a constant function
