English
Let f,g: α → ℝ. If f ≥ 0 eventually, f ≤ g eventually, and g → 0, then f → 0.
Русский
Пусть f,g: α → ℝ. Если f(t) неотрицательно для всех sufficiently далеко, и f(t) ≤ g(t) в достаточно больших t, и g(t) сходится к 0, то и f(t) сходится к 0.
LaTeX
$$$\forall f,g:\,\alpha\to\mathbb{R},\ \forall t_0:\,\mathcal{F}(\alpha),\ (\forall^\infty t\in t_0:\ 0\le f(t)) \\ \land (\forall^\infty t\in t_0:\ 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'` for the
general case. -/
theorem squeeze_zero' {α} {f g : α → ℝ} {t₀ : Filter α} (hf : ∀ᶠ t in t₀, 0 ≤ f t) (hft : ∀ᶠ t in t₀, f t ≤ g t)
(g0 : Tendsto g t₀ (𝓝 0)) : Tendsto f t₀ (𝓝 0) :=
tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds g0 hf hft
