Alphabeta Math
ExampleConstruction: AI-adaptedVerification: AI-generatedSession-authored (Fable 5 assisted)judge pass (z-ai/glm-5.2)audited 2026-07-31
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.

GL1(R)=R∖{0}GL_1(\mathbb{R})=\mathbb{R}\setminus\{0\} is disconnected, whereas R2∖{0}\mathbb{R}^2\setminus\{0\} is polygonally connected

Example

The invertible 1×11\times1 real matrices are the nonzero real numbers, so GL1(R)=R∖{0}GL_1(\mathbb R)=\mathbb R\setminus\{0\}. This set is disconnected: it contains −1-1 and 11 but not the intermediate point 00, so it is not order-convex and cannot be connected by The connected subspaces of R\mathbb{R} with its usual topology are exactly the order-convex subsets, the published characterisation transported by the identification of the two descriptions of "open in R\mathbb{R}". In contrast, For n≥2n\ge2, the punctured space Rn∖{0}\mathbb{R}^n\setminus\{0\} is polygonally connected gives polygonal connectedness of R2∖{0}\mathbb R^2\setminus\{0\}. Connectedness is understood through Separation of a topological space, connected and disconnected spaces, clopen sets, and connected subsets.

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: 100 results over 17 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