tendsto_of_tendsto_of_tendsto_of_le_of_le'

English

There is a TendstoIxxClass structure for Icc with respect to nhds a under OrderTopology.

Русский

Существует структура TendstoIxxClass для Icc относительно nhds a при OrderTopology.

LaTeX

$$$\\text{TendstoIxxClass } Set.Icc (nhds(a)) (nhds(a))$$$

Lean4

/-- **Squeeze theorem** (also known as **sandwich theorem**). This version assumes that inequalities
hold eventually for the filter. -/
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 : ∀ᶠ b in b, g b ≤ f b) (hfh : ∀ᶠ b in b, f b ≤ h b) :
    Tendsto f b (𝓝 a) :=
  (hg.Icc hh).of_smallSets <| hgf.and hfh

Похожие утверждения