Tends-to relation: x→a is not x=a, and does not guarantee that function values converge

Goal and scope

In (ℝ, d(x,y)=|x−y|): (1) prove that the sequence x_n=1+1/n tends to 1 while every term satisfies x_n≠1; (2) for g(x)=1 (x>1) and g(x)=0 (x≤1), prove that g(x_n)→1 along x_n, but lim_{x→1} g(x) does not exist. This shows that x→1 by itself neither requires x to equal 1 nor decides whether function values converge.

Works under MKO assumption a1: the explicit metric structure (ℝ,|x−y|). The standard definitions of sequence limits and ε–δ function limits are used as prerequisites. It does not build Mathlib's Filter.Tendsto, nhds or atTop objects and does not prove their equivalence with the ε–δ definitions; it does not change the canonical MKO or its English edition.

Givens and symbols

• metric_def
• abs_rules
• order_basics
• archimedean
• seq_limit_def
• func_limit_def

• G1 — Structure: the reals ℝ with the metric d(x,y)=|x−y| (assumption a1); target point a=1.
• G2 — The sequence x_n=1+1/n, with n ranging over all positive integers.
• G3 — The function g:ℝ→ℝ with g(x)=1 for x>1 and g(x)=0 for x≤1.

• x\to a — the tends-to relation (directional language)
• x_n — the sequence 1+1/n
• g — the function with a jump at 1
• \varepsilon,\ \delta — tolerances on the target side and on the source side
• N — an index threshold depending on ε
• d(x,y)=|x-y| — the standard metric on ℝ

Rules and sources

• metric_def · prerequisite — Metric: d:X×X→ℝ with d(x,y)≥0 and d(x,y)=0 ⇔ x=y; d(x,y)=d(y,x); triangle inequality d(x,z)≤d(x,y)+d(y,z).
• abs_rules · prerequisite — Absolute value (reals): |u|=u if u≥0 and |u|=−u if u<0; |u|≥0; |uv|=|u||v|; triangle inequality |u+v|≤|u|+|v|; |u|<r ⇔ −r<u<r.
• order_basics · prerequisite — Order of the reals: exactly one of u<v, u=v, u>v holds; u<v and v<w give u<w; u<v gives u+w<v+w; u<v and w>0 give uw<vw; u<v and w<0 give uw>vw.
• archimedean · prerequisite — Archimedean property: for every real x there is a natural number n>x; hence for every ε>0 there is n with 1/n<ε.
• seq_limit_def · prerequisite — Limit of a sequence: a_n→L means that for every ε>0 there is N such that |a_n−L|<ε for all n≥N.
• func_limit_def · prerequisite — Limit of a function: lim_{x→a} f(x)=L means that for every ε>0 there is δ>0 such that |f(x)−L|<ε for every domain point x with 0<|x−a|<δ (a must be a limit point of the domain).
• mul_inverse_nonzero · prerequisite — Inverse of a nonzero number: in ℚ, ℝ or ℂ, if u≠0 there is 1/u with u·(1/u)=1, and v/u means v·(1/u). 0 has no inverse, so v/0 is undefined.
• add_zero · prerequisite — Additive identity: u+0=u.
• forall_intro · prerequisite — ∀-introduction (generalization): if a statement is proved for an arbitrary element x, with no extra assumption on x, it holds for every x in the domain.
• def_unfold · prerequisite — Unfolding a definition: replacing a defined term by its definition (or folding it back) does not change whether a statement is true.
• add_assoc · prerequisite — Associativity of addition: (u+v)+w=u+(v+w).
• add_comm · prerequisite — Commutativity of addition: u+v=v+u.
• add_inverse · prerequisite — Additive inverse: every u has −u with u+(−u)=0; u−v means u+(−v).
• exists_elim · prerequisite — ∃-elimination: from ∃x∈D, P(x) we may name some element a with P(a) by a fresh name; reasoning with a is allowed as long as the final conclusion does not mention a.
• case_analysis · prerequisite — Proof by cases: if P∨Q holds and both P⇒R and Q⇒R are proved, then R holds. The cases must cover every possibility.
• frac_rules · prerequisite — Fraction rules (all denominators nonzero): a/c+b/c=(a+b)/c; (a/b)(c/d)=(ac)/(bd); (a/b)/(c/d)=(ad)/(bc) (also needing c≠0); a/b=(ak)/(bk) for k≠0.
• logic_chain · prerequisite — Chaining: from P⇒Q and Q⇒R infer P⇒R; likewise for ⇔.
• forall_elim · prerequisite — ∀-elimination (instantiation): if ∀x∈D, P(x) holds and a∈D, then P(a) holds.
• two_nonzero · prerequisite — In the reals 0<1, hence 0<1+1=2, so 2≠0.
• modus_ponens · prerequisite — Modus ponens: from P and P⇒Q infer Q.
• eq_replace · prerequisite — Replacement of equals: an expression inside a statement may be replaced by an equal expression without changing whether the statement is true.
• contradiction · prerequisite — Proof by contradiction: if assuming ¬P leads to a contradiction (a statement and its negation both hold), then P holds.
• quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x).
• neg_mul · prerequisite — Signs and multiplication: (−u)v=−(uv) and (−u)(−v)=uv.
• mul_one · prerequisite — Multiplicative identity: 1·u=u.
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• mko_tends_to · cited — The relation x→a is directional language used in limits. By itself it does not say whether function values converge, nor does it require x eventually to equal a. · mko-tends-to-relation
• L_recip_le · lemma — For reals 0<u≤v: 1/v≤1/u.
• L_half · lemma — For a real δ>0: 0<δ/2<δ.
• L_abs_neg · lemma — For a real u: |−u|=|u|.

Main derivation

\text{a structure for nearness}

(\mathbb{R},d),\ d(x,y)=|x-y|,\ a=1

n\ \text{a positive integer}

x_n=1+\tfrac1n>1,\ x_n\neq 1

x_n\to 1

\forall\varepsilon>0\ \exists N\ \forall n\ge N:\ |x_n-1|<\varepsilon

|x_n-1|

\tfrac1n

\varepsilon>0\ \text{arbitrary}

N\in\mathbb{N},\ N>\tfrac1\varepsilon,\ N\ge 1

n\ge N\ge 1

\tfrac1n\le\tfrac1N

N>\tfrac1\varepsilon

\tfrac1N<\varepsilon

|x_n-1|=\tfrac1n\le\tfrac1N<\varepsilon\ \ (n\ge N)

x_n\to 1,\ \text{while}\ x_n\neq 1\ \text{for every}\ n

x_n>1\ \text{for every}\ n

g(x_n)=1\ \text{for every}\ n,\ g(x_n)\to 1

\lim_{x\to 1}g(x)=L

\forall\varepsilon>0\ \exists\delta>0\ \forall x:\ 0<|x-1|<\delta\Rightarrow|g(x)-L|<\varepsilon

\lim_{x\to 1}g(x)=L\ \text{(assumed)},\ \varepsilon=\tfrac12

\delta>0:\ 0<|x-1|<\delta\Rightarrow|g(x)-L|<\tfrac12

p=1+\tfrac\delta2,\ q=1-\tfrac\delta2

0<|p-1|<\delta,\ 0<|q-1|<\delta,\ g(p)=1,\ g(q)=0

\text{S11 applied at}\ x=p\ \text{and}\ x=q

|1-L|<\tfrac12,\ |0-L|<\tfrac12

|1-L|<\tfrac12,\ |0-L|<\tfrac12

1<1\ (\text{contradiction});\ \lim_{x\to 1}g(x)\ \text{does not exist}

x_n\to 1,\ x_n\neq 1,\ g(x_n)\to 1,\ \lim_{x\to 1}g(x)\ \text{does not exist}

x\to 1\ \text{neither forces}\ x=1\ \text{nor decides whether}\ g(x)\ \text{converges}

Substeps and lemmas

0<u\le v

\tfrac1v\le\tfrac1u

\delta>0

0<\tfrac\delta2<\delta

|-u|

|u|

1=|1-0|=|(1-L)+(L-0)|

1\le|1-L|+|0-L|<\tfrac12+\tfrac12=1

Reverse audits

• S15 · sufficient_goal_reduction · S08, S09, S14, mko_tends_to, and_intro_elim — Goal G is the conjunction of the two parts of the problem; each is proved forwards by the listed steps, and this step only forms the conjunction and compares it with the MKO; G is never used as a premise.
• S14.2 · premise_audit · abs_rules, S13, S14.1, order_basics — The triangle inequality is one-way (≤), and adding two strict inequalities gives a strict one; the whole chain only needs one direction.
• S14.1 · inverse_equivalence · abs_rules, neg_mul, mul_one — Each move is an identity and both sides are the same number, so the step holds both ways.
• S14 · premise_audit · S13, contradiction, order_basics — The contradiction comes only from the assumption of S11, so what is refuted is exactly 'the limit exists'; the argument places no restriction on L.
• S13 · premise_audit · S11, S12, forall_elim, eq_replace — Before instantiating, p and q must be shown to satisfy the hypothesis of S11 (S12).
• S12.1 · premise_audit · order_basics, frac_rules — Only multiplication by a positive number and adding the same number to both sides are used; for δ≤0 the conclusion fails.
• S12 · premise_audit · L_half, abs_rules, G3 — δ>0 is needed for 0<δ/2<δ; neither p nor q equals 1, so the punctured condition holds. |−δ/2|=δ/2 uses δ/2>0 and the absolute-value rule.
• S11 · premise_audit · S10, forall_elim, exists_elim — This is the temporary assumption of the proof by contradiction, discharged after S14 reaches a contradiction; δ is a fresh name and the final conclusion does not mention it.
• S10 · inverse_equivalence · func_limit_def — Unfolding the definition holds both ways.
• S09 · premise_audit · S02, G3, seq_limit_def — The conclusion is about this one sequence only; it is not claimed that the limit of g at 1 exists, and S14 proves that it does not.
• S08 · sufficient_goal_reduction · S03, S04, S05, S06, S07, forall_intro — Goal G: x_n→1. Sufficient condition H: for every ε>0 some N gives |x_n−1|<ε for n≥N; H⇒G by S03. H is proved forwards in S04 to S07 with ε arbitrary; G is never used as a premise.
• S07 · premise_audit · order_basics, frac_rules — ε/N>0 is needed to keep the direction of the inequality; this step uses only N>1/ε from S05.
• S06.1 · premise_audit · order_basics, case_analysis, frac_rules — Keeping the direction needs 1/(uv)>0; if u or v could be negative the conclusion may fail (for example u=−1, v=1 gives 1/v=1>−1=1/u).
• S06 · premise_audit · L_recip_le, S05 — The lemma needs u>0, supplied by N≥1 from S05.
• S05 · premise_audit · archimedean, exists_elim — ε>0 is needed for 1/ε to exist; the existence of N is not obtained by trying a few values of ε but is guaranteed for every ε by the Archimedean property.
• S04 · inverse_equivalence · add_inverse, abs_rules, S02 — Both sides are the same number; |u|=u needs u≥0, which S02 supplies as 1/n>0.
• S03 · inverse_equivalence · seq_limit_def — Unfolding and folding back the definition both hold.
• S02 · premise_audit · order_basics, mul_inverse_nonzero — It needs n>0; the conclusion holds for each n because n is an arbitrary positive integer. Only x_n>1 is derived; no converse is claimed.
• S01 · premise_audit · G1, metric_def, abs_rules — This step only fixes the structure and derives no new fact; with another metric or topology, nearness would mean something else.

Error controls and negative controls

x→1 is not x=1

The MKO names the mistake of reading x→a as x=a. The sequence x_n tends to 1, yet every term has x_n>1 (S02, S08). The definition of a function limit even excludes x=1 explicitly (0<|x−1|, S10): the substituted value g(1)=0 is neither the limit 1 along x_n nor a limit at all, since the limit does not exist (S14).

One approach path is not the full definition

The MKO also warns against treating the bare arrow as the full Filter.Tendsto or ε–δ definition. Checking along x_n gives g(x_n)→1 (S09), which covers only one sequence approaching from the right; the ε–δ definition requires every x in the punctured neighbourhood, including the left-hand point q (S12), so the limit does not exist.

The order of quantifiers

A common mistake is turning 'for every ε there is N' into 'there is N for every ε'. The latter fails for x_n: given any N, take ε=1/N and n=N; then |x_N−1|=1/N is not less than ε (N10 shows N=3). The N of S05 depends on ε, which is exactly what the definition allows.

• x_n→1, so some term x_n equals 1 → reject — Every term has x_n=1+1/n>1 (S02).
• g(x_n)→1 along x_n, so lim_{x→1} g(x)=1 → reject — The left-hand point q has g(q)=0; S11 to S14 prove that the limit does not exist.
• x→1 means substituting x=1, so lim_{x→1} g(x)=g(1)=0 → reject — The definition excludes x=1 (S10), and the limit does not exist (S14).
• There is N such that |x_n−1|<ε for all ε>0 and all n≥N → reject — Take ε=1/N and n=N; |x_N−1|=1/N is not less than ε.
• Writing x→1 already says that g(x) converges → reject — The MKO says the tends-to relation by itself does not say whether function values converge; here g has no limit at 1 (S14).

Result and limitations

In (ℝ,|x−y|), x_n=1+1/n tends to 1 while no term equals 1; for the function g with a jump at 1, g(x_n)→1 along x_n, yet lim_{x→1} g(x) does not exist (every candidate L leads to 1<1). So x→1 by itself neither requires x=1 nor decides whether function values converge; a full limit statement also needs a target value, the order of quantifiers and the punctured-neighbourhood condition.

• This guide uses only the ε–N and ε–δ definitions for the metric |x−y|; their correspondence with Mathlib's Filter.Tendsto, nhds and atTop is not proved here.
• N4 checks (1+1/n)−1=1/n only for n from 1 to 50, a finite check; the general case is proved by the addition rules in S04. N1 to N3 and N5 to N11 only check specific numbers, and the argument does not depend on them.

Verification and source binding

11 declared checks for this guide; only the listed expressions are covered.

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: 9cb369c6f946a7068f52b3a1c30a5922a592d1864238416d34c642fcdd014920
• original source SHA-256: 9cb369c6f946a7068f52b3a1c30a5922a592d1864238416d34c642fcdd014920
• Lean: NOT_RUN · independent AI: NOT_MEASURED

Same-source full JSON (formulas, ASTs, controls and revision log)