Mathlib Phrasebook

7.2. Proving limits🔗

You have a limit statement in Tendsto or ∀ᶠ form (see the companion Limit statements entry for how to write one). This entry covers five common recipes (algebraic combination, composition, filter_upwards, EventuallyEq substitution, and unfolding continuity to Tendsto) that handle most everyday goals. Other proofs lean on monotonicity (Filter.Tendsto.mono_left, Filter.Eventually.mono) or on map/comap (see Operations on filters). Stay in the filter world; reach for ε-δ only when translating from classical sources.

7.2.1. Combine two convergent sequences🔗

Algebraic operations on limits are all dot-style on Tendsto:

example {u v : ℕ → ℝ} {a b : ℝ} (hu : Tendsto u atTop (𝓝 a)) (hv : Tendsto v atTop (𝓝 b)) : Tendsto (fun n => u n + v n) atTop (𝓝 (a + b)) := hu.add hv example {u : ℕ → ℝ} {a c : ℝ} (hu : Tendsto u atTop (𝓝 a)) : Tendsto (fun n => c * u n) atTop (𝓝 (c * a)) := tendsto_const_nhds.mul hu

The general pattern: Tendsto.<op> for every algebraic operation that makes sense. Filter.Tendsto.add, Filter.Tendsto.mul, Filter.Tendsto.const_smul, Filter.Tendsto.neg. Constants come from tendsto_const_nhds.

7.2.2. Composition: Tendsto.comp🔗

example : Tendsto (g ∘ f) l₁ l₃ := hg.comp hf

Note the order: hg.comp hf, with the outer function's Tendsto on the left. This matches function composition g ∘ f, not the left-to-right hf then hg order you might expect.

7.2.3. Strengthen an "eventually" fact: filter_upwards🔗

When you have ∀ᶠ x in l, p₁ x and ∀ᶠ x in l, p₂ x and want ∀ᶠ x in l, q x, the tactic is Mathlib.Tactic.filterUpwards:

example {u : ℕ → ℝ} (h1 : ∀ᶠ n in atTop, 0 ≤ u n) (h2 : ∀ᶠ n in atTop, u n ≤ 1) : ∀ᶠ n in atTop, u n ∈ Set.Icc (0 : ℝ) 1 := u:ℕ → ℝh1:∀ᶠ (n : ℕ) in atTop, 0 ≤ u nh2:∀ᶠ (n : ℕ) in atTop, u n ≤ 1⊢ ∀ᶠ (n : ℕ) in atTop, u n ∈ Set.Icc 0 1 filter_upwards [h1, h2] with n u:ℕ → ℝh1:∀ᶠ (n : ℕ) in atTop, 0 ≤ u nh2:∀ᶠ (n : ℕ) in atTop, u n ≤ 1n:ℕhn1:0 ≤ u n⊢ u n ≤ 1 → u n ∈ Set.Icc 0 1 u:ℕ → ℝh1:∀ᶠ (n : ℕ) in atTop, 0 ≤ u nh2:∀ᶠ (n : ℕ) in atTop, u n ≤ 1n:ℕhn1:0 ≤ u nhn2:u n ≤ 1⊢ u n ∈ Set.Icc 0 1 All goals completed! 🐙

The with n hn1 hn2 clause names the bound variable and the strengthened hypotheses; you then prove the pointwise goal q n. This is usually cleaner than combining Eventually.and and Eventually.mono by hand.

7.2.4. Limits depend only on eventual values: EventuallyEq🔗

The Filter.EventuallyEq relation, written f =ᶠ[l] g, means f x = g x holds l-eventually. Anything that only depends on l-eventual behaviour transfers from f to g for free; in particular, Tendsto f l m ↔ Tendsto g l m.

The two lemmas you'll actually reach for:

  • Filter.Tendsto.congr takes Tendsto f l m and f =ᶠ[l] g and produces Tendsto g l m. Use as a one-step rewrite on a Tendsto you already have in hand.

  • Filter.tendsto_congr' is the same fact as an iff, when you want to rewrite both directions.

example {f g : ℕ → ℝ} {a : ℝ} (hf : Tendsto f atTop (𝓝 a)) (hfg : f =ᶠ[atTop] g) : Tendsto g atTop (𝓝 a) := hf.congr' hfg

7.2.5. Continuity at a point as a Tendsto🔗

ContinuousAt f x is Tendsto f (𝓝 x) (𝓝 (f x)):

example (f : X → Y) (x : X) : ContinuousAt f x ↔ Tendsto f (𝓝 x) (𝓝 (f x)) := Iff.rfl

So every limit lemma is a continuity lemma, and vice versa. When proof search for Continuous stalls, unfolding through filters often unblocks it.