Showing changes from revision #4 to #5:
Added | Removed | Changed
Contents
Idea
The decimal numbers as familiar from school mathematics.
Definition
The type of decimal numbers, denoted , is defined as the higher inductive type generated by:
Raw Mathematical ring structures structure on the decimal numbers
Zero Ring structure on the decimal numbers
We define zero to be the following:
Zero
We define zero to be the following:
Addition
We define addition to be the following:
Addition
We define addition to be the following:
for , , , .
Negation
for , , , .
We define negation to be the following:
Negation
We define negation to be the following:
for , .
Subtraction
for , .
We define subtraction to be the following:
Subtraction
We define subtraction to be the following:
for , , , .
One
for , , , .
We define one to be the following:
One
We define one to be the following:
Multiplication
We define multiplication to be the following:
Multiplication
We define multiplication to be the following:
for , , , .
Exponentiation
for , , , .
We define exponentiation to be the following:
Exponentiation
We define exponentiation to be the following:
for , , .
for , , .
Sign
Positive sign
We define the dependent type is positive, denoted as , to be the following:
for , , dependent types indexed by .
Negative sign
We define the dependent type is negative, denoted as , to be the following:
for , , dependent types indexed by .
Zero sign
We define the dependent type is zero, denoted as , to be the following:
for , .
Non-positive sign
We define the dependent type is non-positive, denoted as , to be the following:
for , .
Non-negative sign
We define the dependent type is non-negative, denoted as , to be the following:
for , .
Non-zero sign
We define the dependent type is non-zero, denoted as , to be the following:
for , .
Order structure on the decimal numbers
Less than
We define the dependent type is less than, denoted as , to be the following:
for , , , .
Greater than
We define the dependent type is greater than, denoted as , to be the following:
for , , , .
Apart from
We define the dependent type is apart from, denoted as , to be the following:
for , , , .
Less than or equal to
We define the dependent type is less than or equal to, denoted as , to be the following:
for , , , .
Greater than or equal to
We define the dependent type is greater than or equal to, denoted as , to be the following:
for , , , .
Pseudolattice structure on the decimal numbers
Ramp
We define the ramp function to be the following:
for , , .
Minimum
We define the minimum to be the following:
for , , , .
Maximum
We define the maximum to be the following:
for , , , .
Absolute value
We define the absolute value to be the following:
for , .
Properties
TODO: Show that the decimal numbers are a ordered Heyting integral domain with decidable equality, decidable apartness, and decidable linear order, and that the decimal numbers are a Heyting integral subdomain of the rational numbers.
10 is a unit term.
Thus this is true:
this forms the basis of scientific notation.
See also