surjOn_Iio_of_monotone_surjective

English

Let f be monotone and surjective. Then the image of the ray (−∞, a) under f is (−∞, f(a)).

Русский

Пусть f монотонна и сюръективна. Образ луча (−∞, a) равен (−∞, f(a)).

LaTeX

$$$$\text{SurjOn}(f, Iio(a), Iio(f(a))).$$$$

Lean4

theorem surjOn_Iio_of_monotone_surjective (h_mono : Monotone f) (h_surj : Function.Surjective f) (a : α) :
    SurjOn f (Iio a) (Iio (f a)) :=
  @surjOn_Ioi_of_monotone_surjective _ _ _ _ _ h_mono.dual h_surj a

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