English
Generalized squeeze: if s tends to lb.smallSets and f x ∈ s x eventually, then f tends to lb.
Русский
Обобщённая теорема о зажатии: если s стремится к lb.smallSets, и f(x) ∈ s(x) выполняется упорядочно, тогда f(x) стремится к lb.
LaTeX
$$$ (\\\\forall^\\\\infty x \\\\in la, f(x) \\in s(x)) \\\\Rightarrow \\\\operatorname{Tendsto} f \\\\la lb $$$
Lean4
/-- Generalized **squeeze theorem** (also known as **sandwich theorem**). If `s : α → Set β` is a
family of sets that tends to `Filter.smallSets lb` along `la` and `f : α → β` is a function such
that `f x ∈ s x` eventually along `la`, then `f` tends to `lb` along `la`.
If `s x` is the closed interval `[g x, h x]` for some functions `g`, `h` that tend to the same limit
`𝓝 y`, then we obtain the standard squeeze theorem, see
`tendsto_of_tendsto_of_tendsto_of_le_of_le'`. -/
theorem of_smallSets {s : α → Set β} {f : α → β} (hs : Tendsto s la lb.smallSets) (hf : ∀ᶠ x in la, f x ∈ s x) :
Tendsto f la lb := fun t ht => hf.mp <| (tendsto_smallSets_iff.mp hs t ht).mono fun _ h₁ h₂ => h₁ h₂
