ExampleConstruction: Literature-sourcedVerification: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)verified 2026-07-26 (claude-opus-5)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

$\inf {1 / n : n \geq 1} = 0$ , not attained, while $\sup {1 / n : n \geq 1} = 1$ is

Example

Write $n \cdot 1$ for the canonical natural number $\underset{n}{\underset{⏟}{1 + \dots + 1}}$ of $R$ (Canonical naturals are positive and strictly increasing) and $1 / n : = (n \cdot 1)^{- 1}$ . The set $H = {1 / n : n \geq 1} = {1, 1 / 2, 1 / 3, \dots}$ has $\inf H = 0$ , which is not attained, and $\sup H = 1$ , which is attained, being $\max H$ (Maximum and minimum of a set).

The interesting half is the infimum, and it is exactly the Archimedean property (Every complete ordered field is Archimedean) in disguise. That $0$ is a lower bound is immediate from positivity of the canonical naturals. That no positive number is a lower bound is the statement that the reciprocals of the naturals get below every positive $ε$ , which is what the Archimedean property asserts once applied to $ε^{- 1}$ . Leastness is then read off from the epsilon characterisation Epsilon characterisation of the infimum. Nothing is asserted by inspection: for each $ε > 0$ an explicit index is produced.

Facts & Assumptions

Given: The complete ordered field $R$ ; for a natural number $n \geq 1$ let $n \cdot 1$ denote the canonical natural of $R$ and write $1 / n : = (n \cdot 1)^{- 1}$ ; and let $H : = {1 / n : n \geq 1}$ .

[L1]

Canonical naturals: $1 \cdot 1 = 1$ ; $n \cdot 1 > 0$ for every $n \geq 1$ ; and $n \mapsto n \cdot 1$ is strictly increasing on ${1, 2, 3, \dots}$ , so that $1 = 1 \cdot 1 \leq n \cdot 1$ for every $n \geq 1$ , with equality exactly when $n = 1$ (Canonical naturals are positive and strictly increasing).

[L2]

Archimedean property: $R$ is a complete ordered field, hence Archimedean, so for every $x \in R$ there is a natural $n \geq 1$ with $x < n \cdot 1$ (Every complete ordered field is Archimedean, Archimedean ordered field).

[L3]

Inverses and order: if $a > 0$ then $a^{- 1} > 0$ ; if $0 < a < b$ then $0 < b^{- 1} < a^{- 1}$ (claims 1 and 2 of Inverses of positives are positive, and reciprocation reverses order); and, from uniqueness of the multiplicative inverse, $(a^{- 1})^{- 1} = a$ for every $a \neq 0$ and $1^{- 1} = 1$ , since $a^{- 1} a = 1$ exhibits $a$ as an inverse of $a^{- 1}$ and the identity axiom $1 \cdot x = x$ at $x = 1$ exhibits $1$ as an inverse of itself (Field).

[L4]

Multiplying by a positive constant is an order equivalence: for $c > 0$ one has $x < y$ if and only if $x c < y c$ , and hence, by trichotomy, $x \leq y$ if and only if $x c \leq y c$ (Sign rules for products and monotonicity of multiplication, Ordered field).

[L5]

Epsilon characterisation of the infimum: for a nonempty $X \subseteq R$ bounded below and a lower bound $m$ of $X$ , one has $m = \inf X$ if and only if for every $ε > 0$ there is $x \in X$ with $x < m + ε$ (Epsilon characterisation of the infimum, Greatest lower bound (infimum)).

[L6]

Maximum and attainment: $m = \max X$ means $m \in X$ and $x \leq m$ for all $x \in X$ ; if a nonempty $X$ has a maximum then $\sup X$ exists and $\sup X = \max X$ (Maximum and minimum of a set, The supremum is attained exactly when a maximum exists).

[L7]

Order: trichotomy holds, so $a < a$ is impossible and the negation of $a \leq b$ is $b < a$ ; the order is transitive; and $0 < 1$ (Complete ordered field (least-upper-bound property), Ordered field, The multiplicative identity is positive).

[L8]

Lower bound and bounded below: $ℓ$ bounds $X$ below when $ℓ \leq x$ for all $x \in X$ , and $X$ is bounded below when such an $ℓ$ exists (Lower bound, bounded below, bounded set).

[L9]

Minimum, and the infimum as greatest lower bound: $m = \min X$ means $m \in X$ and $m \leq x$ for all $x \in X$ , so a minimum is a lower bound of $X$ belonging to $X$ (Maximum and minimum of a set); and $\inf X$ is the greatest lower bound, so $ℓ \leq \inf X$ for every lower bound $ℓ$ of $X$ (Greatest lower bound (infimum)).

Verification

technique · direct

1.1

$H$ is nonempty: taking $n = 1$ gives the canonical natural $1 \cdot 1 = 1$ by [L1], and $1 / 1 = 1^{- 1} = 1$ by [L3], so $1 \in H$ .

L1L3

1.2

Every element of $H$ is positive, so $0$ is a lower bound of $H$ and $H$ is bounded below: for $n \geq 1$ one has $n \cdot 1 > 0$ , hence $1 / n = (n \cdot 1)^{- 1} > 0$ and in particular $0 \leq 1 / n$ .

L1L3L8

1.3

Every element of $H$ is $\leq 1$ : fix $n \geq 1$ and multiply by the positive constant $n \cdot 1$ , which by [L4] turns the inequality $(n \cdot 1)^{- 1} \leq 1$ into the equivalent inequality $1 = (n \cdot 1)^{- 1} (n \cdot 1) \leq 1 \cdot (n \cdot 1) = n \cdot 1$ , and the latter holds by [L1].

L1L3L4

1.4

Let $ε > 0$ be arbitrary; then $ε^{- 1} > 0$ , and the Archimedean property applied to $ε^{- 1}$ supplies a natural $n_{ε} \geq 1$ with $ε^{- 1} < n_{ε} \cdot 1$ .

assume-hypL2L3choose

2.1

That index witnesses the approximation: from $0 < ε^{- 1} < n_{ε} \cdot 1$ and [L3] one gets $0 < (n_{ε} \cdot 1)^{- 1} < (ε^{- 1})^{- 1} = ε$ , that is $1 / n_{ε} \in H$ with $1 / n_{ε} < 0 + ε$ .

step 1.4L3L7

2.2

$0 \notin H$ : every element of $H$ is $> 0$ by 1.2, whereas $0 > 0$ is impossible by irreflexivity.

step 1.2L7

2.3

$1 = \max H$ : the element $1$ lies in $H$ by 1.1 and dominates every element of $H$ by 1.3.

step 1.1step 1.3L6

3.1

$H$ is nonempty and bounded below by $0$ , and for every $ε > 0$ some element of $H$ is $< 0 + ε$ ; the epsilon characterisation therefore gives $\inf H = 0$ .

step 1.1step 1.2step 2.1L5

3.2

Since $H$ is nonempty with maximum $1$ , the attainment criterion gives that $\sup H$ exists and $\sup H = \max H = 1 \in H$ .

step 2.3step 1.1L6

4.1

$H$ has no minimum: a minimum of $H$ would be a lower bound of $H$ lying in $H$ , hence at most the greatest lower bound $\inf H = 0$ ; but every element of $H$ is $> 0$ by 1.2, and $x \leq 0$ together with $0 < x$ is impossible by trichotomy.

step 3.1step 1.2L7L9

5.1

Hence $\inf H = 0 \notin H$ and $\sup H = 1 \in H$ : the infimum of $H$ is not attained and $H$ has no minimum, while the supremum is attained and is the maximum.

step 3.1step 3.2step 2.2step 4.1L6∎

Remarks

The set $H$ is bounded, with $0 \leq h \leq 1$ for every $h \in H$ , and its members are pairwise distinct, since $n \mapsto 1 / n$ is strictly decreasing on ${1, 2, 3, \dots}$ : for $n < m$ the map $n \mapsto n \cdot 1$ is strictly increasing by [L1], so $0 < n \cdot 1 < m \cdot 1$ , and inversion reverses that by [L3], giving $1 / m < 1 / n$ . It is the standard example showing that a bounded set with infinitely many members can attain one of its two bounds and miss the other. ("Infinite" is used here in its everyday sense: no definition of finiteness is in scope on this page, and nothing above or below depends on one.)
Positivity of every element is what makes $0$ a lower bound, and the Archimedean property is what makes it the greatest one. In a non-Archimedean ordered field the argument breaks at exactly one point, step 1.4: it is the Archimedean property (Every complete ordered field is Archimedean) that supplies, for a given $ε > 0$ , an index $n_{ε}$ with $ε^{- 1} < n_{ε} \cdot 1$ , and hence with $1 / n_{ε} < ε$ in step 2.1. And Not every ordered field is Archimedean exhibits an ordered field where no such natural exists. What that item establishes is the failure of the Archimedean property there; it says nothing about $H$ or its greatest lower bound, and this page does not compute one. So the value $\inf H = 0$ is a statement about $R$ , not a formal manipulation.
Read as a sequence rather than a set, $H$ is the classical null sequence; the rational form of the same fact is The sequence $1 / n$ is null.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

23 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Archimedean property (Wikipedia) (standard reference, not scraped)
Infimum and supremum (Wikipedia) (standard reference, not scraped)
W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 1 (standard reference, not scraped)
T. Tao, Analysis I, 3rd ed. (standard reference, not scraped)
John K. Hunter, An Introduction to Real Analysis (standard reference, not scraped)

inf⁡{1/n:n≥1}=0inf{1/n:n≥1}=0, not attained, while sup⁡{1/n:n≥1}=1sup{1/n:n≥1}=1 is