English
Let f be monotone and surjective between linearly ordered α and partially ordered β. If a ≤ b, then the image of the closed interval [a, b] under f covers the closed interval [f(a), f(b)].
Русский
Пусть f монотонна и сюръективна между линейно упорядоченными множества α и β. Если a ≤ b, то образ отрезка [a, b] покривает отрезок [f(a), f(b)].
LaTeX
$$$$\text{SurjOn}(f, Icc(a,b), Icc(f(a),f(b))).$$$$
Lean4
theorem surjOn_Icc_of_monotone_surjective (h_mono : Monotone f) (h_surj : Function.Surjective f) {a b : α}
(hab : a ≤ b) : SurjOn f (Icc a b) (Icc (f a) (f b)) :=
by
intro p hp
rcases eq_endpoints_or_mem_Ioo_of_mem_Icc hp with (rfl | rfl | hp')
· exact ⟨a, left_mem_Icc.mpr hab, rfl⟩
· exact ⟨b, right_mem_Icc.mpr hab, rfl⟩
· exact image_mono Ioo_subset_Icc_self <| surjOn_Ioo_of_monotone_surjective h_mono h_surj a b hp'
