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.
A supremum need not belong to its set:
Statement refuted
Refuted claim: if is nonempty and bounded above then ; equivalently, every nonempty subset of that is bounded above has a maximum (FALSE: the supremum of a set belongs to the set, Maximum and minimum of a set).
The witness is the open unit interval . It is nonempty, it is bounded above by , its supremum exists and equals , and . The supremum computation is carried out in full in and , with neither attained and is not repeated here; this item records only what that computation refutes.
Facts & Assumptions
Given: The complete ordered field and the open interval .
The open unit interval: is nonempty, is an upper bound of , , and ( and , with neither attained).
Attainment: for a nonempty whose supremum exists, holds exactly when has a maximum, and then (The supremum is attained exactly when a maximum exists, Maximum and minimum of a set).
The refuted claim: for every nonempty that is bounded above, exists and (FALSE: the supremum of a set belongs to the set).
Order: trichotomy holds, so is impossible (Complete ordered field (least-upper-bound property), Ordered field).
Counterexample
is a nonempty subset of bounded above by , so it is an instance of the claim, and its supremum exists with .
: membership in requires , and is impossible by irreflexivity.
Hence and , so and the claim fails on .
Equivalently, has no maximum: a maximum of would have to be and would have to lie in , and does not.
The open unit interval is therefore a nonempty, bounded above subset of whose supremum exists and does not belong to it; the claim that a supremum belongs to its set is refuted, and so is the equivalent claim that boundedness above forces a maximum.
Remarks
- The false statement FALSE: the supremum of a set belongs to the set carries its own self-contained refutation with the same witness. This item exists so that the computation and the refutation are separated: and , with neither attained establishes the value from the epsilon characterisation, and the refutation is then a two-line consequence of it.
- What survives of the claim is exactly The supremum is attained exactly when a maximum exists: the supremum lies in the set precisely when a maximum exists. A sufficient condition is being nonempty and finite (Every nonempty finite set of reals has a maximum and a minimum); finiteness alone is not sufficient, since is finite and has no maximum (Maximum and minimum of a set). And and is the attaining companion of this witness, with the same supremum.
- Nothing about is special beyond being open at the top. Any set whose supremum is approached but not reached does the same job, which is why the supremum, and not the maximum, is the right notion for analysis.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 27 results over 9 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.
Sources
- Infimum and supremum (Wikipedia) (standard reference, not scraped)
- Maximum and minimum (Wikipedia) (standard reference, not scraped)
- W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 1 (standard reference, not scraped)
- John K. Hunter, An Introduction to Real Analysis (standard reference, not scraped)