surjOn_Ici_of_monotone_surjective

English

Let f be monotone and surjective. For any a, the image of the closed interval [a, ∞) under f is [f(a), ∞).

Русский

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

LaTeX

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

Lean4

theorem surjOn_Ici_of_monotone_surjective (h_mono : Monotone f) (h_surj : Function.Surjective f) (a : α) :
    SurjOn f (Ici a) (Ici (f a)) := by
  rw [← Ioi_union_left, ← Ioi_union_left]
  exact (surjOn_Ioi_of_monotone_surjective h_mono h_surj a).union_union (@image_singleton _ _ f a ▸ surjOn_image _ _)

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