English
If a function is continuous on a nonempty interval s and the restriction tends to the bottom along atBot and to the top along atTop, then it is surjective onto the entire codomain.
Русский
Если функция непрерывна на непустом интервале s и ограничение стремится к дну при atBot и к верху при atTop, то она сюръективна на всю область значений.
LaTeX
$$SurjOn f s univ$$
Lean4
/-- A continuous function which tendsto `Filter.atTop` along `Filter.atTop` and to `atBot` along
`at_bot` is surjective. -/
theorem surjective {f : α → δ} (hf : Continuous f) (h_top : Tendsto f atTop atTop) (h_bot : Tendsto f atBot atBot) :
Function.Surjective f := fun p =>
mem_range_of_exists_le_of_exists_ge hf (h_bot.eventually (eventually_le_atBot p)).exists
(h_top.eventually (eventually_ge_atTop p)).exists
