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

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-tends-to-relation/)

This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented.

derivation-mko-tends-to-relation-01 · production-20261019-adopted-96



## 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

S01 · definitionBefore

\text{a structure for nearness}

After

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

Conditions: none

Rule: metric_def · Uses: G1

Leaf basis: metric_def + abs_rules

By MKO assumption a1, a structure supporting nearness must be specified before approach is discussed. Take ℝ with the metric d(x,y)=|x−y|: it is nonnegative, zero only when x=y, symmetric, and satisfies the triangle inequality (abs_rules). The target point is a=1. From here on 'close to 1' means that |x−1| is small.



S02 · impliesBefore

n\ \text{a positive integer}

After

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

Conditions: n>0

Rule: order_basics · Uses: G2

Leaf basis: order_basics + mul_inverse_nonzero + add_zero + forall_intro

For every positive integer n, 1/n>0 (the reciprocal of a positive number is positive: if 1/n≤0, multiplying by n>0 would give 1≤0, a contradiction). By the additive order property, x_n=1+1/n>1+0=1, so x_n≠1. No term of the sequence equals 1.



S03 · equivalentBefore

x_n\to 1

After

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

Conditions: none

Rule: seq_limit_def · Uses: S01, G2

Leaf basis: seq_limit_def + def_unfold

Unfold x_n→1 by the definition of the limit of a sequence. Note the order of quantifiers: ε is given first and arbitrary, then N is found (N may depend on ε), and then the distance must be less than ε for all n≥N. Nothing in the definition requires x_n=1.



S04 · equivalentBefore

|x_n-1|

After

\tfrac1n

Conditions: \tfrac1n>0

Rule: abs_rules · Uses: G2, S02

Leaf basis: add_assoc + add_comm + add_inverse + add_zero + abs_rules

x_n−1=(1+1/n)−1=1/n (associativity and inverses for addition). Since 1/n>0 (S02), the absolute-value rule gives |1/n|=1/n. So the distance from x_n to 1 is exactly 1/n.



S05 · impliesBefore

\varepsilon>0\ \text{arbitrary}

After

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

Conditions: \varepsilon>0

Rule: archimedean · Uses: S03

Leaf basis: archimedean + exists_elim + mul_inverse_nonzero

Take any ε>0; then 1/ε is a positive real. By the Archimedean property there is a natural number N>1/ε; since 1/ε>0, N>0 and so N≥1. N depends on ε: the smaller ε, the larger the N needed. For example, with ε=1/10 we have 1/ε=10 and may take N=11.



S06 · impliesBefore

n\ge N\ge 1

After

\tfrac1n\le\tfrac1N

Conditions: N>0

Rule: L_recip_le · Uses: S05

Leaf basis: order_basics + case_analysis + mul_inverse_nonzero

By Lemma L_recip_le (proved in S06.1) with u=N and v=n: from 0<N≤n we get 1/n≤1/N. As the index increases, the distance 1/n does not increase.



S07 · impliesBefore

N>\tfrac1\varepsilon

After

\tfrac1N<\varepsilon

Conditions: \varepsilon>0; N>0

Rule: order_basics · Uses: S05

Leaf basis: order_basics + frac_rules + mul_inverse_nonzero

ε/N>0 (a quotient of positive numbers). Multiply both sides by the positive number ε/N: the left side gives N·(ε/N)=ε and the right side (1/ε)·(ε/N)=1/N, so ε>1/N, that is 1/N<ε.



S08 · impliesBefore

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

After

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

Conditions: none

Rule: forall_intro · Uses: S02, S03, S04, S06, S07

Leaf basis: order_basics + forall_intro + logic_chain

For each n≥N: |x_n−1|=1/n (S04) ≤1/N (S06) <ε (S07), so by transitivity of order |x_n−1|<ε. ε was an arbitrary positive number and N comes from S05, so by ∀-introduction the right side of S03 holds and x_n→1. Combined with S02: x_n tends to 1, yet no term equals 1.



S09 · impliesBefore

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

After

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

Conditions: none

Rule: seq_limit_def · Uses: S02, G3

Leaf basis: seq_limit_def + abs_rules + forall_intro

By S02 each x_n>1, so by G3, g(x_n)=1. For any ε>0 take N=1: every n has |g(x_n)−1|=|0|=0<ε, so g(x_n)→1. Along this one sequence approaching 1, the function values converge to 1.



S10 · equivalentBefore

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

After

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

Conditions: none

Rule: func_limit_def · Uses: G3, S01

Leaf basis: func_limit_def + def_unfold

A function limit needs far more data than the bare arrow x→1: a target value L, the order of quantifiers (ε before δ), and the punctured-neighbourhood condition 0<|x−1|<δ (x=1 itself is excluded, so the value g(1) does not affect the limit). 1 is a limit point of the domain ℝ, so the definition applies.



S11 · impliesBefore

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

After

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

Conditions: none

Rule: exists_elim · Uses: S10

Leaf basis: forall_elim + exists_elim

For a proof by contradiction, temporarily assume some real L has lim_{x→1} g(x)=L. Apply the definition S10 with ε=1/2 (∀-elimination) to obtain some δ>0 (∃-elimination, with the fresh name δ) such that every x with 0<|x−1|<δ has |g(x)−L|<1/2.



S12 · impliesBefore

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

After

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

Conditions: \delta>0

Rule: L_half · Uses: S11, G3

Leaf basis: order_basics + abs_rules + frac_rules

Take p=1+δ/2 and q=1−δ/2. |p−1|=δ/2 and |q−1|=|−δ/2|=δ/2. By Lemma L_half (proved in S12.1), 0<δ/2<δ, so p and q both lie in the punctured neighbourhood. Also p>1 and q<1, so by G3, g(p)=1 and g(q)=0. For example, with δ=1/4, p=9/8 and q=7/8, both at distance 1/8<1/4 from 1.



S13 · impliesBefore

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

After

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

Conditions: none

Rule: forall_elim · Uses: S11, S12

Leaf basis: forall_elim + modus_ponens + eq_replace

Both p and q satisfy 0<|x−1|<δ (S12), so instantiate the universal statement of S11 at x=p and at x=q: |g(p)−L|<1/2 and |g(q)−L|<1/2; then substitute g(p)=1 and g(q)=0.



S14 · impliesBefore

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

After

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

Conditions: none

Rule: contradiction · Uses: S13, L_abs_neg

Leaf basis: contradiction + order_basics + abs_rules + quantifier_negation

The computations in S14.1 and S14.2 give 1<1, contradicting trichotomy of order. So the temporary assumption of S11 fails: no real L has lim_{x→1} g(x)=L, that is the limit does not exist. L was arbitrary, so the conclusion covers every candidate value.



S15 · impliesBefore

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

After

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

Conditions: none

Rule: mko_tends_to · Uses: S08, S09, S14

Leaf basis: mko_tends_to + and_intro_elim

Collect and compare with the MKO: (1) x_n→1 while every x_n≠1 (S02, S08), so approaching does not require equality; (2) near the same point 1, the function values converge along x_n (S09) but the full ε–δ limit does not exist (S14), so the bare arrow x→1 by itself does not decide whether function values converge; to claim convergence one must also specify the target value, the order of quantifiers and the punctured-neighbourhood condition (S10).







## Substeps and lemmas

S06.1 · impliesBefore

0<u\le v

After

\tfrac1v\le\tfrac1u

Conditions: u>0; v>0

Rule: order_basics · Uses: order_basics

Leaf basis: order_basics + case_analysis + frac_rules + mul_inverse_nonzero

Two cases. If u=v, then 1/v=1/u. If u<v: since u, v>0, 1/(uv)>0, and multiplying both sides by the positive number 1/(uv) keeps the inequality, u·1/(uv)<v·1/(uv), that is 1/v<1/u. Together the cases give 1/v≤1/u, proving Lemma L_recip_le.



S12.1 · impliesBefore

\delta>0

After

0<\tfrac\delta2<\delta

Conditions: \delta>0

Rule: order_basics · Uses: order_basics

Leaf basis: order_basics + frac_rules + two_nonzero

Multiplying δ>0 by the positive number 1/2 gives δ/2>0. Also δ−δ/2=δ/2>0, and adding δ/2 to both sides gives δ>δ/2. This proves Lemma L_half.



S14.1 · equivalentBefore

|-u|

After

|u|

Conditions: none

Rule: abs_rules · Uses: abs_rules

Leaf basis: abs_rules + neg_mul + mul_one

|−u|=|(−1)u|=|−1|·|u| (by |uv|=|u||v|). Since −1<0, |−1|=−(−1)=1, so |−u|=1·|u|=|u|. This proves Lemma L_abs_neg, used next for |L−0|=|−(0−L)|=|0−L|.



S14.2 · impliesBefore

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

After

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

Conditions: none

Rule: abs_rules · Uses: S13, S14.1

Leaf basis: abs_rules + add_inverse + order_basics + numeric_evaluation

1=|1−0|, and 1−0=(1−L)+(L−0) (inserting −L+L=0). By the triangle inequality, |(1−L)+(L−0)|≤|1−L|+|L−0|; by L_abs_neg, |L−0|=|0−L|. With the two inequalities of S13: |1−L|+|0−L|<1/2+1/2=1. Altogether 1<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=1The 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 definitionThe 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 quantifiersA 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)](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-tends-to-relation-01.json)