Homotopy Type Theory Dedekind cut structure real numbers > history (changes)

Showing changes from revision #3 to #4: Added | Removed | Changed

Dedekind cut structure real numbers

< Dedekind cut structure

Large Dedekind cut structure real numbers

The 𝒰\mathcal{U}-large Dedekind cut structure real numbers for a universe 𝒰\mathcal{U} is defined as the type of all pairs of subtypes of the rational numbers \mathbb{Q} which have a 𝒰\mathcal{U}-Dedekind cut structure:

𝒰 (L,R):Sub 𝒰()×Sub 𝒰()[DedekindCutStructure 𝒰(L,R)]\mathbb{R}_\mathcal{U} \coloneqq \sum_{(L, R):Sub_\mathcal{U}(\mathbb{Q}) \times Sub_\mathcal{U}(\mathbb{Q})} \left[DedekindCutStructure_\mathcal{U}(L, R)\right]

Sigma-Dedekind cut structure real numbers

The Σ\Sigma-Dedekind cut structure real numbers for a $\sigma$-frame Σ\Sigma is defined as the type of all pairs of open subtypes of the rational numbers \mathbb{Q} which have a Σ\Sigma-Dedekind cut structure:

Σ (L,R):(Σ)×(Σ)[DedekindCutStructure Σ(L,R)]\mathbb{R}_\Sigma \coloneqq \sum_{(L, R):(\mathbb{Q} \to \Sigma) \times (\mathbb{Q} \to \Sigma)} \left[DedekindCutStructure_\Sigma(L, R)\right]

See also

References

Last revised on June 10, 2022 at 10:36:25. See the history of this page for a list of all contributions to it.