English
If a nonempty ordered connected set s and a continuous f on s satisfy the proper tail conditions, then f maps s onto the whole codomain.
Русский
Пусть существующий не пустой связанный по порядку множество s и непрерывна f на s, удовлетворяющая условиям пределов, тогда образ f на s равен всей области значения.
LaTeX
$$SurjOn f s univ$$
Lean4
/-- If a function `f : α → β` is continuous on a nonempty interval `s`, its restriction to `s`
tends to `at_bot : Filter β` along `at_bot : Filter ↥s` and tends to `Filter.atTop : Filter β` along
`Filter.atTop : Filter ↥s`, then the restriction of `f` to `s` is surjective. We formulate the
conclusion as `Function.surjOn f s Set.univ`. -/
theorem surjOn_of_tendsto {f : α → δ} {s : Set α} [OrdConnected s] (hs : s.Nonempty) (hf : ContinuousOn f s)
(hbot : Tendsto (fun x : s => f x) atBot atBot) (htop : Tendsto (fun x : s => f x) atTop atTop) : SurjOn f s univ :=
haveI := Classical.inhabited_of_nonempty hs.to_subtype
surjOn_iff_surjective.2 <| hf.restrict.surjective htop hbot
