surjOn_Ico_of_monotone_surjective

English

Let f be monotone and surjective. Then for any a,b, SurjOn f (Ico a b) (Ico (f a) (f b)).

Русский

Пусть f монотонна и сюрьективна. Тогда для любых a,b верна последовательность образов: SurjOn f (Ico a b) (Ico (f a) (f b)).

LaTeX

$$$\operatorname{SurjOn} f\ (\mathrm{Ico}\ a\ b)\ (\mathrm{Ico}\ (f a)\ (f b))$$$

Lean4

theorem surjOn_Ico_of_monotone_surjective (h_mono : Monotone f) (h_surj : Function.Surjective f) (a b : α) :
    SurjOn f (Ico a b) (Ico (f a) (f b)) :=
  by
  obtain hab | hab := lt_or_ge a b
  · intro p hp
    rcases eq_left_or_mem_Ioo_of_mem_Ico hp with (rfl | hp')
    · exact mem_image_of_mem f (left_mem_Ico.mpr hab)
    · exact image_mono Ioo_subset_Ico_self <| surjOn_Ioo_of_monotone_surjective h_mono h_surj a b hp'
  · rw [Ico_eq_empty (h_mono hab).not_gt]
    exact surjOn_empty f _

Похожие утверждения