Help proving lim_{x->inf} 1/x = 0

Stream: Is there code for X?

[Jonathan Crall]

I'm learning how to use lean4 and to get started I wanted to try and prove that lim_{x->inf} 1/x = 0 (this is actually just a piece of what I'm trying to prove, but it is that I'm having most trouble with). I've found that Mathlib.Order.Filter.Tendsto is probably what I want to encode the notion of a limit, but I was having trouble using it. I started to attempt to prove something simpler: lim_{x -> 2} x * 3 = 6, but I'm not quite sure how to go about it. Seeing an example might help me understand better. (Also is there a way to directly use the epsilon-delta definition of a limit instead of Tendsto, or are they fundamentally the same?)

If it simplifies things, I'm quite happy working in the Rational numbers instead of the Reals. In fact, even if I have a proof for the Reals, I'd like to additionally prove the special case for Rationals - especially if it leads to simplifications of the proof.

If this is not the best place to ask questions like these please direct me to a better forum for my question.

[Mario Carneiro]

Could you show a minimal example of the code you have? #mwe

[Mario Carneiro]

Using the rationals instead of the reals will most likely make your job harder, not easier, because the reals are complete but the rationals aren't

[Mario Carneiro]

but I guess if you want to prove a specific limit and not just an existence claim then it's probably about the same

[Mario Carneiro]

(note: there is no file called Mathlib.Order.Filter.Tendsto, this confused me slightly about your post. The file is called Mathlib.Order.Filter.Basic and it defines a notion called Filter.Tendsto)

[Mario Carneiro]

I am surprised that

import Mathlib

open Filter
example : Tendsto (fun x => 1/x) atTop (nhds (0:ℝ)) := by exact?

turns up empty, and apply?doesn't seem to have anything relevant. I'm sure this is already in the library

[Mario Carneiro]

on the other hand

example : Tendsto (fun x => x⁻¹) atTop (nhds (0:ℝ)) := by exact?

does work, and suggests docs#tendsto_inv_atTop_zero

[Mario Carneiro]

apparently there isn't a similar result about a / x like I would have expected

[Mario Carneiro]

@Jonathan Crall

[Jonathan Crall]

Thank you, this is very helpful. I'm still getting used to the syntax and import system, hence the incorrect usage of terminology. Your correction makes the distinction between files and the symbols they expose more clear (however I'm still a bit confused about how open Filter can work if you just import Mathlib - how does it know about Filter if Filter is defined in Mathlib.Order?)

For a MWE example... working is a very generous description. I figured out enough to make

import Mathlib.Data.Rat.Defs
def reciprocal (x : Rat) : Rat := 1 / x
#eval reciprocal ((10 + 1))

work

but my limit code that I've tried so far is nonsense:

import Mathlib.Order.Filter.Basic
import Mathlib.Order.Filter.AtTopBot
import Mathlib.Topology.Basic
import Mathlib.Data.Real.Basic
import Mathlib.Analysis.PSeries
import Mathlib.Data.Real.Pi.Wallis

#check Rat
#check Filter.Tendsto
#check Filter.atTop

theorem Real.tendsto_sum_pi_div_four :
Filter.Tendsto (fun k => Finset.sum (Finset.range k) fun i => (-1) ^ i / (2 * ↑i + 1)) Filter.atTop (nhds (Real.pi / 4))

#eval Filter.Tendsto (λ x : Rat => 2 * x) (3) (6)

#check nhds
#check Real.Pi

I was just trying to get a grasp on the concepts. I'm a computer scientist by trade, topology and pure maths is very new to me.

Attempting your code, I had to add in a few imports, but I'm still getting errors:

import «Myfirstproof»
import Mathlib.Order.Filter.Basic
import Mathlib.Topology.Basic
import Mathlib.Data.Real.Basic

open Filter

example : Tendsto (fun x => x⁻¹) atTop (nhds (0:ℝ)) := by exact?

I get:

Main.lean:8:40
failed to synthesize instance
  TopologicalSpace ℝ
Main.lean:8:58
`exact?` could not close the goal. Try `apply?` to see partial suggestions.

It seems upset about (nhds (0:ℝ) and exact?

(Note this is in a vscode environment and I created the project with

elan default stable
elan run --install stable lake new myfirstproof
cd /home/joncrall/code/paper-g1-and-mcc/myfirstproof
lake update
lake exe cache get
lake build

I think I also did some manual modifications to add

require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git"

to lakefile.lean in the myfirstproof directory.

[Mario Carneiro]

import Mathlib means import everything

[Mario Carneiro]

imports are transitive

[Mario Carneiro]

and Mathlib.lean imports every file

[Mario Carneiro]

By importing only Mathlib.Order.Filter.Basic, Mathlib.Topology.Basic and Mathlib.Data.Real.Basic you have imported enough to make sense of the statement but not the proof. The theorem suggested by exact?, tendsto_inv_atTop_zero, lives in Mathlib.Topology.Algebra.Order.Field which is a more advanced file that imports all three of the above files and then adds some more stuff. import Mathlib is just importing the whole library so everything is in there somewhere

[Mario Carneiro]

(Actually you haven't imported enough to make sense of the statement, you need to import whatever provides the instance of TopologicalSpace ℝ. That is, you can't use "the real numbers" and "limits" in the same sentence until you know that the reals are a topological space, and the basic file defining the real numbers doesn't do that)

[Jonathan Crall]

Mario Carneiro said:

imports are transitive

Toto, I have a feeling we're not in coding in Python anymore.

When I run your code verbatim:

import Mathlib
open Filter
example : Tendsto (fun x => x⁻¹) atTop (nhds (0:ℝ)) := by exact?

It takes a ton of CPU and time and then ultimately returns:

`/home/joncrall/.elan/toolchains/stable/bin/lake print-paths Init Mathlib` failed:

stderr:
info: [1440/1492] Building Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
info: [1498/1562] Building Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
info: [1667/1701] Building Mathlib.Algebra.Homology.Homotopy
info: [1668/1709] Building Mathlib.Algebra.Homology.Opposite
info: [1773/1819] Building Mathlib.Algebra.Module.PID
info: [2004/2085] Building Mathlib.Analysis.NormedSpace.PiLp
info: [2092/2183] Building Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
info: [2111/2201] Building Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
info: [2138/2247] Building Mathlib.FieldTheory.IsAlgClosed.Basic
info: [2424/2711] Building Mathlib.Geometry.Manifold.ContMDiff
info: [2750/3000] Building Mathlib.Computability.TMToPartrec
info: [2963/3242] Building Mathlib.FieldTheory.PerfectClosure
info: [3143/3784] Building Mathlib.RingTheory.RootsOfUnity.Minpoly
info: [3172/3787] Building Mathlib.RingTheory.IsAdjoinRoot
info: [3324/3787] Building Mathlib.RingTheory.Perfection
info: [3376/3787] Building Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
info: [3394/3787] Building Mathlib.RepresentationTheory.Action
info: [3415/3787] Building Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
info: [3421/3787] Building Mathlib.Probability.Notation
info: [3441/3787] Building Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
info: [3442/3787] Building Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
info: [3452/3787] Building Mathlib.Probability.Kernel.CondDistrib
error: > LEAN_PATH=./lake-packages/std/build/lib:./lake-packages/Qq/build/lib:./lake-packages/aesop/build/lib:./lake-packages/Cli/build/lib:./lake-packages/proofwidgets/build/lib:./lake-packages/mathlib/build/lib:./build/lib LD_LIBRARY_PATH=./lake-packages/std/build/lib:./lake-packages/Qq/build/lib:./lake-packages/aesop/build/lib:./lake-packages/Cli/build/lib:./lake-packages/proofwidgets/build/lib:./lake-packages/mathlib/build/lib:./build/lib:/home/joncrall/.elan/toolchains/stable/lib/lean:/home/joncrall/.elan/toolchains/stable/lib:./lake-packages/mathlib/build/lib /home/joncrall/.elan/toolchains/stable/bin/lean -Dpp.unicode.fun=true -Dpp.proofs.withType=false -DautoImplicit=false -DrelaxedAutoImplicit=false ./lake-packages/mathlib/././Mathlib/Analysis/NormedSpace/PiLp.lean -R ./lake-packages/mathlib/./. -o ./lake-packages/mathlib/build/lib/Mathlib/Analysis/NormedSpace/PiLp.olean -i ./lake-packages/mathlib/build/lib/Mathlib/Analysis/NormedSpace/PiLp.ilean -c ./lake-packages/mathlib/build/ir/Mathlib/Analysis/NormedSpace/PiLp.c
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5

# Lots more text here

info: [3645/3787] Building Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
info: [3648/3787] Building Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
error: > LEAN_PATH=./lake-packages/std/build/lib:./lake-packages/Qq/build/lib:./lake-packages/aesop/build/lib:./lake-packages/Cli/build/lib:./lake-packages/proofwidgets/build/lib:./lake-packages/mathlib/build/lib:./build/lib LD_LIBRARY_PATH=./lake-packages/std/build/lib:./lake-packages/Qq/build/lib:./lake-packages/aesop/build/lib:./lake-packages/Cli/build/lib:./lake-packages/proofwidgets/build/lib:./lake-packages/mathlib/build/lib:./build/lib:/home/joncrall/.elan/toolchains/stable/lib/lean:/home/joncrall/.elan/toolchains/stable/lib:./lake-packages/mathlib/build/lib /home/joncrall/.elan/toolchains/stable/bin/lean -Dpp.unicode.fun=true -Dpp.proofs.withType=false -DautoImplicit=false -DrelaxedAutoImplicit=false ./lake-packages/mathlib/././Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean -R ./lake-packages/mathlib/./. -o ./lake-packages/mathlib/build/lib/Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.olean -i ./lake-packages/mathlib/build/lib/Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.ilean -c ./lake-packages/mathlib/build/ir/Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.c
error: stdout:
./lake-packages/mathlib/././Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean:225:8: error: tactic 'rewrite' failed, did not find instance of the pattern in the target expression
  (IsOpenMap.functor _).obj ⊤
case h'
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso P
X Y : Scheme
f : X ⟶ Y
U : ↑(Scheme.affineOpens Y)
H :
  ∀ (U_1 : ↑(Scheme.affineOpens (Scheme.restrict X _))),
    P
      (f.val.c.app (op ↑U) ≫
        X.presheaf.map (eqToHom _).op ≫ (Scheme.ofRestrict (Scheme.restrict X _) _).val.c.app (op ⊤))
V : ↑(Scheme.affineOpens X)
e : ↑V ≤ (Opens.map f.val.base).obj ↑U
U' : Opens ↑↑X.toPresheafedSpace := (Opens.map f.val.base).obj ↑U
e' : (IsOpenMap.functor _).obj ((Opens.map (Opens.inclusion U')).obj ↑V) = ↑V
⊢ (Opens.map (Scheme.ofRestrict X _).val.base).obj ↑V ∈ Scheme.affineOpens (Scheme.restrict X _)
error: external command `/home/joncrall/.elan/toolchains/stable/bin/lean` exited with code 1

./lake-packages/mathlib/././Mathlib/Analysis/NormedSpace/PiLp.lean:422:31: error: Declaration PiLp.aux_uniformity_eq not found.
...

[Mario Carneiro]

oh dear, this is one of the things that you have to learn which is mathlib specific

[Mario Carneiro]

use lake exe cache get to download precompiled mathlib

[Mario Carneiro]

(you should have mentioned that it was building before waiting an hour, this would have saved you the effort!)

[Mario Carneiro]

the errors are not expected though, my guess is that your lean-toolchain doesn't match mathlib, which can cause compile failures

[Mario Carneiro]

use cp lake-packages/mathlib/lean-toolchain lean-toolchain to fix this

[Mario Carneiro]

if it works, lake build should take a few seconds to run, not an hour

[Patrick Massot]

@Jonathan Crall, from this and https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Links.20to.20Resources.20for.20Help, I think you took a wrong start in your Lean adventures. If you are interested in Lean for mathematics you should start learning it using a math-oriented resource. If you go to #mil you will find links to installation instructions that work for maths as well as explanation about limits.

[Kevin Buzzard]

I agree with Patrick. The theorem that 1/n tends to 0 needs all sorts of things like facts about how division plays with inequalities, that natural numbers are nonnegative, that for every real number there's a natural number bigger than it and so on. You can of course battle your way through this if you know how to find your way around the library, but it's not the best exercise for a complete beginner (it looks much easier than it is, from a formal perspective). A much better exercise is to prove that the sum of the limits is the limit of the sums; this is what I do in lecture 2 of my undergraduate lean course and even this has some content. I won't recommend my course to you because it's not yet been translated into lean 4 but like Patrick I will recommend #mil .

[Jonathan Crall]

@Mario Carneiro Following your instructions worked. It took about a minute, but it got there. Many thanks.

My interest in using lean is to provide a formal proof for a relationship I found between the MCC and FM measures of a confusion matrix namely the FM is the limit of the MCC as the true negative count tends to infinity. I've written it up here: https://arxiv.org/abs/2305.00594 and I'm fairly sure the informal proof is correct, I've also verified it with sympy, but that only goes so far. Prooving lim_{x -> inf} 1/x = 0 is the main step.

Mathematics in Lean (MIL) looks very helpful. Thank you for the pointer.

EDIT: I forgot the proof also includes a square root operation, so proving it in the rationals wont be possible without modification (or maybe if I restrict to algebreic numbers that would be easier?).

[Ming Li]

With the code and the idea about the real line, how to find the related data from Mathlib? or how to modify the code so that lean can give useful suggestion? "unexpected token 'fun'; expected '_' or identifier" is given here.

Mario Carneiro said:

on the other hand

example : Tendsto (fun x => x⁻¹) atTop (nhds (0:ℝ)) := by exact?

does work, and suggests docs#tendsto_inv_atTop_zero

[Alex J. Best]

What is the whole file that gives you that error message?
If I do

import Mathlib

open Filter

example : Tendsto (fun x => x⁻¹) atTop (nhds (0:ℝ)) := by exact?

I don't see any issues

[Ming Li]

Thanks. I fixed the issue caused by /--/.
Alex J. Best said:

What is the whole file that gives you that error message?
If I do

import Mathlib

open Filter

example : Tendsto (fun x => x⁻¹) atTop (nhds (0:ℝ)) := by exact?

I don't see any issues

[Ming Li]

Are MIL and Mathlib4 compatible to each other? In general, how to merge two libraries?

Patrick Massot said:

Jonathan Crall, from this and https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Links.20to.20Resources.20for.20Help, I think you took a wrong start in your Lean adventures. If you are interested in Lean for mathematics you should start learning it using a math-oriented resource. If you go to #mil you will find links to installation instructions that work for maths as well as explanation about limits.

[Ruben Van de Velde]

MIL depends on mathlib: https://github.com/leanprover-community/mathematics_in_lean

Not sure what you mean by "merge" in this context

[Ming Li]

Thanks for reply. By "merge", I mean that suppose there is another tototial like MIL, also depending on mathlib4 and lean4, how can I use both in a single *.lean file?

Ruben Van de Velde said:

MIL depends on mathlib: https://github.com/leanprover-community/mathematics_in_lean

Not sure what you mean by "merge" in this context

[Ruben Van de Velde]

Yes, you can do that. You should make sure that the versions match up, though

[Ming Li]

Simply moving library folder dose not work. Any suggestion?

[Alex Altair]

@Mario Carneiro @Jonathan Crall I'm just jumping into the middle of this, but surely one doesn't need to involve topology for the limit of 1/x? From browsing the docs, I see this lemma, which seems like the same thing but without topology

[Mario Carneiro]

@Alex Altair The definition of tendsto doesn't involve topology, but usually the next step will. atTop needs an ordering on the type, and nhds is a topological filter

[Mario Carneiro]

so that statement does involve topology

[Jireh Loreaux]

I'm curious why you think "surely one doesn't need to involve topology for the limit of 1/x?" Or why you think docs#IsROrC.tendsto_inverse_atTop_nhds_0_nat didn't use topology.

[Kevin Buzzard]

The definition of tendsto might strictly speaking not involve topology, but it either involves epsilons and deltas or it involves filters, and both of those are topology in disguise (the filter is a topological neighbourhood filter in the application)

[Alex Altair]

I see, that makes sense

[Alex Altair]

@Jireh Loreaux One reason is that limits were understood hundreds of years before people had a concept of topology, and even formalized long before, via the epsilon-delta stuff (in the mid-1800s I think?). We also teach limits before topology, and I don't think calculus classes are sweeping foundations under the rug when they do so without using any language like "open set"

[Alex Altair]

(I didn't realize docs#IsROrC.tendsto_inverse_atTop_nhds_0_nat used topology just because I didn't see the word "topology" anywhere on the page, and I don't have any familiarity with how Mathlib is structured yet)

[Patrick Massot]

I think we need more context to help you. If you are teaching first year undergrads and want to use limits of sequences of real numbers or functions from real numbers to real numbers then clearly you should redefine limits in elementary terms, just like in the tutorial project or in GlimpseOfLean. But if you want to contribute to a full scale math library like mathlib then it makes no sense.

[Jireh Loreaux]

Aha, yes, that makes sense. I think here the point is that the structure of mathlib is relevant. In general, within mathlib, we opt for the most general (modulo convenience and some other considerations) setting possible. So, although limits were originally formulated by Cauchy with ε > 0, ..., that definition doesn't work in more general settings. Instead, convergence (to a point) makes sense in topological spaces. However, because we want to allow even more generality (e.g., aₙ → ∞ as n → ∞), we encapsulate limits in terms of filters, and then convergence to a point x in a topological space is encoded using the neighborhood filter 𝓝 x (i.e., docs#nhds), which is defined in terms of the topology.

For a nice description of why we work in this generality, have a look at Patrick's ICERM talk from last year: https://icerm.brown.edu/video_archive/?play=2899 So, it doesn't have anything to do with wanting to avoid "sweeping foundations under the rug", but rather, with usability, feasibility and convenience.

As Patrick mentioned, this generality isn't suitable for presentation to early undergraduates, so if you are teaching you probably want to roll your own (even if the definitions are connected to Mathlib's docs#Filter.Tendsto behind the curtain).

[Ming Li]

Does it mean that mathlib4 is research oriented while tutorials like GlimpseOfLean is educational one?

[Patrick Massot]

GlimpseOfLean is an introduction to Lean. You can start with it and then learn about the mathlib way in #mil which requires a much larger time investment.

[Ming Li]

Indeed, both are great for beginners. So the particular tactics are designed for educational purpose. They will not be used in Mathlib4, right?

[Gabor Nyeki]

Mario Carneiro said:

on the other hand

example : Tendsto (fun x => x⁻¹) atTop (nhds (0:ℝ)) := by exact?

does work, and suggests docs#tendsto_inv_atTop_zero

When I try this, I get a typeclass error:

import Mathlib

example : Filter.Tendsto (fun (x : ℝ) => x⁻¹) atTop (nhds 0) := by
  refine tendsto_inv_atTop_zero

typeclass instance problem is stuck, it is often due to metavariables
  OrderTopology ?m.721

Why is ℝ not recognized as an instance of OrderTopology?

[Gabor Nyeki]

The error disappears if I also add open Filter.

[Yongyi Chen]

atTop is actually Filter.atTop. Without open Filter, Lean was interpreting it as an implicit variable.

[Anatole Dedecker]

If you want to disable this (it can be very annoying sometimes) you can add set_option autoImplicit false at the beginning of the file

[Alex Altair]

Today I was trying to understand how to work with limits in Lean, and encountered a confusion that is related to this thread (although in a somewhat different direction)

[Alex Altair]

I’m used to limits in standard written mathematics as having a “type” that is something like a real number (or whatever the elements of your topology are, I guess). But it seems like in Lean, they are of type Prop (as in, Filter.TendsTo returns a thing of type Prop). How would you then convert this into a number, so that you can use it in calculations or equations? For example, sometimes we want to use the fact that lim (f(x) + b) = (lim f(x)) + b

[Alex Altair]

Is there some basic lemma I’m missing, or is there a totally different way I should be thinking about limits in Lean?

[Ruben Van de Velde]

Does it help to think of that equality as "if f x tends to l, then f x + b tends to l + b"?

[Jireh Loreaux]

You can state that fact:

import Mathlib

open Topology Filter

noncomputable section

-- a literal translation of your statement
example (f : ℝ → ℝ) (a b : ℝ) : limUnder (𝓝 a) (f · + b) = limUnder (𝓝 a) f + b := sorry

-- a completely arbitrary value of `ℝ`.
example : ℝ := limUnder ⊥ (0 : ℝ → ℝ)

-- another completely arbitrary value of `ℝ`
example : ℝ := limUnder (𝓝 0) (fun x ↦ Real.sin (1 / x))

-- if `f` tends to `L` along the filter `l`, then the limit of `f` along `l` is `L`.
example (f : ℝ → ℝ) (l : Filter ℝ) [l.NeBot] (L : ℝ) (hf : Tendsto f l (𝓝 L)) : limUnder l f = L :=
  hf.limUnder_eq

However, I would caution that often statements involving docs#limUnder are not what you want. The point is basically this: in many cases you don't actually want to extract the value from a limit (which is what docs#limUnder does). Instead, you generally just want to know that if some sequence x n converges to y, then x n + b converges to y + b. Note that both of these are propositions, not data (i.e., values). This latter statement is encoded in the library as docs#Filter.Tendsto.add_const.

[Alex Altair]

Thanks, I think that does help somewhat. Let me see if I understand your examples. For limUnder ⊥ (0 : ℝ → ℝ), does that mean "the limit as x goes to negative infinity of the constant function 0"? In which case, the limit exists and is uniquely zero? And then for the sin(1/x) example, the limit doesn't exist, right? So what would that expression represent?

[Alex Altair]

I see that the docs say, "If [stuff], then limUnder f g is a limit of g at f, if it exists." What is it if the limit doesn't exist?

[Alex Altair]

I could buy that most of the time we don't care to "extract" the value of the limit, though I do feel like a lot of mathematics is concerned about exactly when limits exist and when they're unique

[Jireh Loreaux]

Alex Altair said:

For limUnder ⊥ (0 : ℝ → ℝ), does that mean "the limit as x goes to negative infinity of the constant function 0"?

No, that would be limUnder atBot (0 : ℝ → ℝ). In my example, that ⊥ : Filter ℝ, which is the filter consisting of all sets in ℝ. This is a completely arbitrary value of ℝ because the function 0 : ℝ → ℝ converges to anything along the filter ⊥. limUnder picks an arbitrary value when there are multiple limits.

[Jireh Loreaux]

Alex Altair said:

What is it if the limit doesn't exist?

An arbitrarily chosen value in ℝ (chosen with docs#Classical.choice)

[Jireh Loreaux]

This is why it's not terribly useful.

[Jireh Loreaux]

Alex Altair said:

though I do feel like a lot of mathematics is concerned about exactly when limits exist and when they're unique

sure, we still care about this in formalization too. However, the way we phrase "this limit exists" is often different. We simply say Tendsto (f : ℝ → ℝ) (𝓝 a) (𝓝 b) to say what we phrase in informal language as f(x) → b as a x → a.

And indeed, we also care about uniqueness. For example, it's often the case that you want to say b = c because they are the both limits of the same function. You can do this with docs#tendsto_nhds_unique.

[Jireh Loreaux]

(@Alex Altair I edited the first message above because I was correct in my original example. I just momentarily confused myself.)

[Jireh Loreaux]

Let's get down to practical considerations for a moment. The following is taken directly from a conversation I had with my students in introductory real analysis. Let's say f : ℝ → ℝ is some function, but morally its domain is D : Set ℝ. So, what is a limit of f as x approaches a : ℝ? Their textbook requires, in order for this limit to be defined, that a is an accumulation point of D (that is , AccPt a D). Why do they do this? Well, because if you expand the usual definition of limit, you would get: ∀ ε > 0, ∃ δ > 0, ∀ x : ℝ, x ∈ (ball a δ ∖ {a}) ∩ D → f x ∈ ball L ε (this say that the limit of f as x appproaches a is L). Now, if a is not an accumulation point, then there is some δ > 0 such that ball a δ ∖ {a} = ∅, in which case the above statement would be true regardless of the value of L. This would mean that a is not an accumulation point of D, then *for any L : ℝ, f converges to L as x approaches a. Presumably, the textbook wanted to preserve uniqueness of limits, so they don't allow this scenario by definition.

However, this is very inconvenient. It means for example, that you can't say that f is continuous on D iff the limit of the function f at each point a ∈ D is f a. You can't do this because if a is an isolated point of D, then the right-hand side isn't even defined. That's stupid and annoying, and I said as much to my class.

[Jireh Loreaux]

As another practical example, that hopefully addresses your original question, consider the following. I have f x approaches L as x approaches a, and f x + b approaches L' as x approaches a. Then I can conclude L' = L + b.

import Mathlib

open Topology Filter

example (f : ℝ → ℝ) (a b L' L : ℝ) (hf : Tendsto f (𝓝[≠] a) (𝓝 L)) (hf' : Tendsto (f · + b) (𝓝[≠] a) (𝓝 L')) :
    L' = L + b :=
  tendsto_nhds_unique hf' <| hf.add_const b

[Alex Altair]

Thank you very much! The concreteness really helps

[Alex Altair]

As an aside, why did you include [≠] in the most recent example? (It looks like the proof still goes through without it)

[Jireh Loreaux]

Sure, it does. In fact, it will work with any filter other than ⊥. I only included it as this was the filter I was using implicitly in the remarks above (with δ).