English
Squeeze-type lemma: if g→a and h→a, and g ≤ f ≤ h eventually, then f→a.
Русский
Лемма типа прижима: если g и h стремятся к a, и g ≤ f ≤ h почти наверняка, то f стремится к a.
LaTeX
$$$\\mathrm{Tendsto}(g,b,nhds(a)) \\land \\mathrm{Tendsto}(h,b,nhds(a)) \\land (\\forall^{\\infty} b, g(b) \\le f(b)) \\land (\\forall^{\\infty} b, f(b) \\le h(b)) \\Rightarrow \\mathrm{Tendsto}(f,b,nhds(a))$$$
Lean4
/-- **Squeeze theorem** (also known as **sandwich theorem**). This version assumes that inequalities
hold everywhere. -/
theorem tendsto_of_tendsto_of_tendsto_of_le_of_le [OrderTopology α] {f g h : β → α} {b : Filter β} {a : α}
(hg : Tendsto g b (𝓝 a)) (hh : Tendsto h b (𝓝 a)) (hgf : g ≤ f) (hfh : f ≤ h) : Tendsto f b (𝓝 a) :=
tendsto_of_tendsto_of_tendsto_of_le_of_le' hg hh (Eventually.of_forall hgf) (Eventually.of_forall hfh)
