Rolle's theorem to Taylor's theorem

• Rolle's theorem

TheoremSqueeze theorem#

Squeeze theorem (also known as sandwich theorem). This version assumes that inequalities hold eventually for the filter.

tendsto_of_tendsto_of_tendsto_of_le_of_le'.{u, v} {α : Type u} {β : Type v}
  [ts : TopologicalSpace α] [Preorder α] [OrderTopology α] {f g h : β → α} {b : Filter β} {a : α}
  (hg : Filter.Tendsto g b (nhds a)) (hh : Filter.Tendsto h b (nhds a))
  (hgf : ∀ᶠ (b : β) in b, g b ≤ f b) (hfh : ∀ᶠ (b : β) in b, f b ≤ h b) :
  Filter.Tendsto f b (nhds a)

Sources

• Mathlib documentation: tendsto_of_tendsto_of_tendsto_of_le_of_le'
• Source of tendsto_of_tendsto_of_tendsto_of_le_of_le' in Mathlib/Topology/Order/Basic.lean
• 1000+ theorems list: Q1065257
• 1000+ theorems project: Q1065257
• Wikipedia: Squeeze theorem
• Wikidata: Q1065257

Mathlibtendsto_of_tendsto_of_tendsto_of_le_of_le'

Uses 3 · Used by 9

Statement usesLimit of a map with respect to filters · Order topology

Proof usesNatural number

Used byL’Hopital’s Rule · Fubini's theorem · Banach open mapping theorem · Completeness of spaces of bounded continuous functions · Translation numbers define a group action up to semiconjugacy · Fourier theorem · Lebesgue's decomposition theorem · Lévy continuity theorem · Hilbert projection theorem

• Stirling's theorem
• Taylor's theorem

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.