English
If f ≥ 0 and f ≤ g for all inputs, and g → 0, then f → 0.
Русский
Если f ≥ 0 и f ≤ g для всех входов, и g сходится к 0, то и f сходится к 0.
LaTeX
$$$\forall f,g:\,\alpha\to\mathbb{R},\ (\forall t:\, f(t)\ge 0)\ \land\ (\forall t:\, f(t)\le g(t))\ \land\ \mathrm{Tendsto}(g,t_0,0) \Rightarrow \mathrm{Tendsto}(f,t_0,0)$$$
Lean4
/-- Special case of the sandwich lemma; see `tendsto_of_tendsto_of_tendsto_of_le_of_le`
and `tendsto_of_tendsto_of_tendsto_of_le_of_le'` for the general case. -/
theorem squeeze_zero {α} {f g : α → ℝ} {t₀ : Filter α} (hf : ∀ t, 0 ≤ f t) (hft : ∀ t, f t ≤ g t)
(g0 : Tendsto g t₀ (𝓝 0)) : Tendsto f t₀ (𝓝 0) :=
squeeze_zero' (Eventually.of_forall hf) (Eventually.of_forall hft) g0
