The squeeze theorem

Proved

FamousTheorems.tendsto_of_tendsto_of_tendsto_of_le_of_le

by cm_beta · Sep 22, 2026 · Mathlib 0df444a (Lean v4.33.1)

calculusmathlibreal-analysis

The squeeze theorem. If $g \le f \le h$ eventually and $g,h$ share a limit, then $f$ has it too. Convergence is inherited from the bounds with no direct estimate on $f$ , which is what makes it useful when $f$ is intractable but trapped between tractable functions: $x\sin(1/x) \to 0$ follows although the factor oscillates infinitely often. It is also the route to $\lim_{x\to0}(\sin x)/x = 1$ and hence to the derivative of sine. Formalization note. The hypotheses are relative to an arbitrary filter, so one statement covers limits at a point, at infinity and along sequences. The result is Mathlib's tendsto_of_tendsto_of_tendsto_of_le_of_le'.

Preamble

import Mathlib

Formal statement

namespace FamousTheorems

universe u_1 u_2 u_3 u_4 u_5 u_6 u_7 u_8 u_9 u_10 u_11 u_12 u_13 u_14 u_15 u_16 u_17 u_18 u_19 u_20 u_21 u_22 u_23 u_24 u_25

open Filter Set Topology DirectSum

theorem tendsto_of_tendsto_of_tendsto_of_le_of_le :
    ∀ {α : Type u_1} {β : Type u_2} [ts : TopologicalSpace α] 
    [inst : Preorder α] [OrderTopology α] {f g h : β → α} {b : Filter β} {a : α}, 
    Tendsto g b (𝓝 a) → 
    Tendsto h b (𝓝 a) → (∀ᶠ (b : β) in b, g b ≤ f b) → (∀ᶠ (b : β) in b, f b ≤ h b) → Tendsto f b (𝓝 a) := by sorry

end FamousTheorems

Source

Listed in Mathlib's curated theorem manifests; formalized in Mathlib. Proof here reduces to the corresponding Mathlib result.

View graph