English
If f is continuous on s and the reindexed dual order meets the same tail conditions with reversed orientation, then surjectivity holds.
Русский
Если 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 `Filter.atTop : Filter β` along `Filter.atBot : Filter ↥s` and tends to
`Filter.atBot : 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 atTop) (htop : Tendsto (fun x : s => f x) atTop atBot) : SurjOn f s univ :=
ContinuousOn.surjOn_of_tendsto (δ := δᵒᵈ) hs hf hbot htop
