Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passverified 2026-08-02 (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.

Inclusion totally orders the Dedekind reals

Statement

Set inclusion totally orders the Dedekind reals (Order on the Dedekind reals): the relation A≤B:⇔A⊆B on cuts (Dedekind cut) is reflexive, antisymmetric (with antisymmetry delivering set equality A=B), and transitive, and it is moreover total: for any two cuts A,B, either A⊆B or B⊆A.

Facts & Assumptions

Given: Dedekind cuts A,B∈R, ordered by inclusion (Order on the Dedekind reals).

[A1]

Set inclusion ⊆ is a partial order on any family of sets: reflexive (A⊆A), antisymmetric (mutual inclusion A⊆B, B⊆A gives A=B), and transitive.

[A2]

The order on Q is total (The rationals form a totally ordered field): for rationals x,y exactly one of x<y, x=y, y<x holds.

[L1]

Downward closure (C2): if p∈A and q<p then q∈A, and likewise for B (Dedekind cut).

Proof

technique · direct
1.1

The relation ≤ is set inclusion, and ⊆ is reflexive, antisymmetric (mutual inclusion A⊆B and B⊆A forces the set equality A=B), and transitive; hence ≤ is a partial order on R.

A1
1.2

It remains to establish totality. Fix cuts A,B; if A⊆B there is nothing to prove, so assume A⊈B. It suffices to show B⊆A.

suffices: B ⊆ A when A ⊄ B
2.1

Since A⊈B, choose a rational x with x∈A and x∉B.

step 1.2choose
3.1

Every y∈B satisfies y<x: otherwise x≤y by trichotomy, and then downward closure of B places x∈B (directly if x<y, or as x=y∈B), contradicting x∉B.

step 2.1L1A2
4.1

Fix any y∈B. From y<x together with x∈A, downward closure of A gives y∈A; as y∈B was arbitrary, B⊆A.

step 2.1step 3.1L1
5.1

Thus for all cuts A,B, A⊆B or B⊆A, so ≤ is total; combined with the partial-order properties, set inclusion is a total order on R.

step 1.1step 1.2step 4.1∎

Depends on

Used by

Dependency tree · two levels

9 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