nLab streak

Definition

In constructive mathematics, given a $\sigma$-locale $\Sigma$ whose poset of opens $O(\Sigma)$ is a $\sigma$-frame, a $\Sigma$-streak is an archimedean difference protoring $M$ such that the strict total order $\lt:M \times M \to \Omega$ factors into $\lt^{'}:M \times M \to \Sigma$ and the canonical monotone $i:\Sigma \to \Omega$, where $\Omega$ is the subset classifier. $\Sigma$ is typically called the open subset classifier.

Examples

• For any $\sigma$-locale $\Sigma$, the Dedekind real numbers are the terminal $\Sigma$-streak.

• For any $\sigma$-locale $\Sigma$, the $\Sigma$-Dedekind real numbers are a $\Sigma$-streak.

See also

• archimedean difference protoring

• Dedekind cut

• Dedekind real numbers

• number line rig

References

• Davorin Lešnik, Synthetic Topology and Constructive Metric Spaces, (arxiv:2104.10399)