English
Special case of the sandwich theorem: if the norm of f is eventually bounded by a real function a which tends to 0, then f tends to 1.
Русский
Особый случай теоремы sandwich: если норма f в конечном итоге ограничена вещественной функцией a, которая стремится к 0, тогда f → 1.
LaTeX
$$Tendsto f t (nhds 1) given the bound and tendsto of a$$
Lean4
/-- Special case of the sandwich theorem: if the norm of `f` is bounded by a real function `a` which
tends to `0`, then `f` tends to `1`. -/
@[to_additive /-- Special case of the sandwich theorem: if the norm of `f` is bounded by a real
function `a` which tends to `0`, then `f` tends to `0`. -/
]
theorem squeeze_one_norm {f : α → E} {a : α → ℝ} {t₀ : Filter α} (h : ∀ n, ‖f n‖ ≤ a n) :
Tendsto a t₀ (𝓝 0) → Tendsto f t₀ (𝓝 1) :=
squeeze_one_norm' <| Eventually.of_forall h
