Dependencies

A sequence \(x \colon \mathrm{MyNat}\to \mathrm{MyRat}\) is a Cauchy sequence if

Every Cauchy sequence \(x\) is bounded: there exists \(B {\gt} 0\) such that \(|x_n| \leq B\) for all \(n\).

We define our integers \(\mathrm{MyInt}\) as

We will write \(⟦ (a, b) ⟧\) for the class of \((a,b)\).

We define the addition of \(x = ⟦ (a, b) ⟧\) and \(y = ⟦ (c, d) ⟧\) in \(\mathrm{MyInt}\) as

Thanks to Lemma 33 this is well defined.

Addition on \(\mathrm{MyInt}\) is associative.

Let \(x\), \(y\) and \(z\) in \(\mathrm{MyInt}\) be such that \(x \leq y\). Then \(x + z \leq y + z\).

For every \(x\) in \(\mathrm{MyInt}\) there exists \(n\) in \(\mathrm{MyNat}\) such that \(x \leq i(n)\).

\(\mathrm{MyInt}\) with addition and multiplication is a commutative ring.

Let \(x\), \(y\) and \(z\) in \(\mathrm{MyInt}\) such that \(x \neq 0\) and \(y * x = z * x\). Then \(y = z\).

We define a map

For all \(a\) and \(b\) in \(\mathrm{MyNat}\) we have that

We have that \(i\) is injective.

Given two natural numbers \(a\) and \(b\), we have \(i(a) \leq i(b)\) if and only if \(a \leq b\).

For all \(a\) and \(b\) in \(\mathrm{MyNat}\) we have that

We have that \(i(1) = 1\).

We have that \(i(0) = 0\).

Let \(x\) and \(y\) in \(\mathrm{MyInt}\). We write \(x \leq y\) if there exist a natural number \(n\) such that

The relation \(\leq \) on \(\mathrm{MyInt}\) is antisymmetric.

The relation \(\leq \) on \(\mathrm{MyInt}\) is reflexive.

The order \(\leq \) on \(\mathrm{MyInt}\) is a total order.

The relation \(\leq \) on \(\mathrm{MyInt}\) is transitive.

We have that \(\mathrm{MyInt}\) with \(\leq \) is a linear order

We define the multiplication of \(x = ⟦ (a, b) ⟧\) and \(y = ⟦ (c, d) ⟧\) in \(\mathrm{MyInt}\) as

Thanks to Lemma 35 this is well defined.

Let \(x\) and \(y\) in \(\mathrm{MyInt}\) such that \(x \neq 0\) and \(y \neq 0\). Then \(x*y \neq 0\).

Let \(x\) and \(y\) in \(\mathrm{MyInt}\) be such that \(0 {\lt} x\) and \(0 {\lt} y\). Then \(0 {\lt} x * y\).

We define the negation of \(x = ⟦ (a, b) ⟧\) in \(\mathrm{MyInt}\) as

Thanks to Lemma 31 this is well defined.

We define the one of \(\mathrm{MyInt}\), denoted \(1\) as the class of \((1,0)\).

We define the zero of \(\mathrm{MyInt}\), denoted \(0\) as the class of \((0,0)\).

In \(\mathrm{MyInt}\) we have that \(0 \leq 1\).

In \(\mathrm{MyInt}\) we have \(0 \neq 1\).

We define \(\mathrm{MyNat}\) as the inductive type with two constructors:

• a term \(0\) (called zero);

• for every \(n \in \mathrm{MyNat}\), a term \(\mathrm{succ}(n)\) (the successor of \(n\)).

In other words, every natural number is obtained from \(0\) by applying the successor function a finite number of times. We write \(1\) for \(\mathrm{succ}(0)\).

We define addition on \(\mathrm{MyNat}\) by recursion on the second argument:

Addition on \(\mathrm{MyNat}\) is associative.

Addition on \(\mathrm{MyNat}\) is commutative.

Let \(a\), \(b\) and \(c\) in \(\mathrm{MyNat}\) be such that \(a \leq b\). Then \(a + c \leq b + c\).

\(\mathrm{MyNat}\) with addition and multiplication is a commutative semiring.

Let \(a\) and \(b\) in \(\mathrm{MyNat}\). We write \(a \leq b\) if there exists a natural number \(x\) such that

The relation \(\leq \) on \(\mathrm{MyNat}\) is antisymmetric.

The relation \(\leq \) on \(\mathrm{MyNat}\) is reflexive.

The order \(\leq \) on \(\mathrm{MyNat}\) is total.

The relation \(\leq \) on \(\mathrm{MyNat}\) is transitive.

For all \(a\), \(b\) and \(c\) in \(\mathrm{MyNat}\) we have \(a * (b + c) = a * b + a * c\).

We have that \(\mathrm{MyNat}\) with \(\leq \) is a linear order.

We define multiplication on \(\mathrm{MyNat}\) by recursion on the second argument:

Multiplication on \(\mathrm{MyNat}\) is associative.

Multiplication on \(\mathrm{MyNat}\) is commutative.

Let \(a\), \(b\) and \(c\) in \(\mathrm{MyNat}\) be such that \(0 {\lt} c\) and \(a {\lt} b\). Then \(c * a {\lt} c * b\).

Let \(a\), \(b\) and \(c\) in \(\mathrm{MyNat}\) be such that \(0 {\lt} c\) and \(a {\lt} b\). Then \(a * c {\lt} b * c\).

Let \(a\) and \(b\) in \(\mathrm{MyNat}\) be such that \(a \neq 0\) and \(b \neq 0\). Then \(a * b \neq 0\).

For all \(a\) in \(\mathrm{MyNat}\) we have \(1 * a = a\).

For all \(a\), \(b\) and \(c\) in \(\mathrm{MyNat}\) we have \((a + b) * c = a * c + b * c\).

For all \(a\) in \(\mathrm{MyNat}\) we have \(0 + a = a\).

In \(\mathrm{MyNat}\) we have \(0 \neq 1\).

Let \(\mathrm{MyPreint}\) be \(\mathrm{MyNat}\times \mathrm{MyNat}\).

We define an operation, called addition on \(\mathrm{MyPreint}\) as follows: the addition of \(x = (a,b)\) and \(y = (c, d)\) is

If \(x \approx x'\) and \(y \approx y'\), then \(x + y \approx x' + y'\).

We define an operation, called multiplication on \(\mathrm{MyPreint}\) as follows: the multiplication of \(x = (a,b)\) and \(y = (c, d)\) is

If \(x \approx x'\) and \(y \approx y'\), then \(x * y \approx x' * y'\).

We define an operation, called negation on \(\mathrm{MyPreint}\) as follows: the negation of \(x = (a,b)\) is \((b,a)\):

If \(x \approx x'\), then \(-x \approx -x'\).

We define a relation \(R\) on \(\mathrm{MyPreint}\) as follows: \((a,b)\) and \((c, d)\) are related if and only if

We have that \(R\) is an equivalence relation. From now on, we will write \(x \approx y\) for \(x R y\).

\(R\) is a reflexive relation.

\(R\) is a symmetric relation.

\(R\) is a transitive relation.

Let \(\mathrm{MyPrerat}\) be \(\mathrm{MyInt}\times (\mathrm{MyInt}\setminus \{ 0\} )\).

We define an operation, called addition on \(\mathrm{MyPrerat}\) as follows: the addition of \(x = (a,b)\) and \(y = (c, d)\) is

Do you see why it is well defined?

If \(x \approx x'\) and \(y \approx y'\), then \(x + y \approx x' + y'\).

We define an operation, called inversion on \(\mathrm{MyPrerat}\) as follows: the inverse of \(x = (a,b)\) is:

Note that \(x^{-1}\) is always defined!

If \(x \approx x'\), then \(x^{-1} \approx x'^{-1}\).

We define an operation, called multiplication on \(\mathrm{MyPrerat}\) as follows: the multiplication of \(x = (a,b)\) and \(y = (c, d)\) is

If \(x \approx x'\) and \(y \approx y'\), then \(x * y \approx x' * y'\).

We define an operation, called negation on \(\mathrm{MyPrerat}\) as follows: the negation of \(x = (a,b)\) is \((-a,b)\):

Note that it is automatically well defined (meaning that second component of \((-a,b)\) is different from \(0\)).

If \(x \approx x'\), then \(-x \approx -x'\).

We define a relation \(R\) on \(\mathrm{MyPrerat}\) as follows: \((a,b)\) and \((c, d)\) are related if and only if

We have that \(R\) is an equivalence relation. From now on, we will write \(x \approx y\) for \(x R y\).

\(R\) is a reflexive relation.

\(R\) is a symmetric relation.

\(R\) is a transitive relation.

Let \(\mathrm{MyPrereal}\) be the type of Cauchy sequences, that is the subtype of \(x \colon \mathrm{MyNat}\to \mathrm{MyRat}\) such that \(x\) is a Cauchy sequence.

If \(x \approx x'\) and \(y \approx y'\), then \(x + y \approx x' + y'\).

Let \(x\) be in \(\mathrm{MyPrereal}\) such that both \(x\) and \(-x\) are nonnegative. Then \(x \approx 0\).

We define the inverse of \(x\) in \(\mathrm{MyPrereal}\) as the termwise inverse \(x^{-1}\) if \(x \not\approx 0\), and as \(0\) otherwise. Note that it is always defined.

If \(x \approx x'\), then \(x^{-1} \approx x'^{-1}\).

If \(x\) and \(y\) are Cauchy sequences, then \(x + y\) (the termwise sum) is a Cauchy sequence. In particular addition is well defined on \(\mathrm{MyPrereal}\).

For any rational \(x\), the constant sequence \(n \mapsto x\) is a Cauchy sequence.

Let \(x\) be in \(\mathrm{MyPrereal}\) with \(x \not\approx 0\). Then the termwise inverse \(x^{-1}\) is a Cauchy sequence.

If \(x\) and \(y\) are Cauchy sequences, then \(x * y\) (the termwise product) is a Cauchy sequence. In particular multiplication is well defined on \(\mathrm{MyPrereal}\).

If \(x\) is a Cauchy sequence, then \(-x\) (the termwise negation) is a Cauchy sequence. In particular negation is well defined on \(\mathrm{MyPrereal}\).

Given \(x\) in \(\mathrm{MyPrereal}\), we say that \(x\) is nonnegative if either \(x\) is positive or \(x \approx 0\).

Let \(x\) be in \(\mathrm{MyPrereal}\) such that \(x\) is not nonnegative. Then \(-x\) is nonnegative.

If \(x \approx 0\), then \(x\) is nonnegative.

If there exists \(N\) such that \(0 \leq x_n\) for all \(n \geq N\), then \(x\) is nonnegative.

If \(x \approx x'\) and \(x\) is nonnegative, then \(x'\) is nonnegative.

Given \(x\) in \(\mathrm{MyPrereal}\), we say that \(x\) is positive if there exist \(\delta {\gt} 0\) and \(N\) such that \(\delta \leq x_n\) for all \(n \geq N\), in other words if \(x\) is eventually bounded below by a positive rational.

Let \(x\) and \(y\) in \(\mathrm{MyPrereal}\) both positive. Then \(x + y\) is positive.

Let \(x\) and \(y\) in \(\mathrm{MyPrereal}\) both positive. Then \(x * y\) is positive.

If \(x \approx x'\) and \(x\) is positive, then \(x'\) is positive.

If \(x \approx x'\) and \(y \approx y'\), then \(x * y \approx x' * y'\).

If \(x \approx x'\), then \(-x \approx -x'\).

If \(x\) is positive, then \(x \not\approx 0\).

If \(x \approx 0\), then \(x\) is not positive.

We define the one of \(\mathrm{MyPrereal}\) as the constant sequence \(1\).

The one of \(\mathrm{MyPrereal}\) is nonnegative.

The one of \(\mathrm{MyPrereal}\) is positive.

If \(x\) is positive, then there exists \(N\) such that \(0 {\lt} x_n\) for all \(n \geq N\).

Let \(x\) be in \(\mathrm{MyPrereal}\) with \(x \not\approx 0\). Then there exist \(\delta {\gt} 0\) and \(N\) such that \(\delta {\lt} |x_n|\) for all \(n \geq N\).

We define a relation \(R\) on \(\mathrm{MyPrereal}\) as follows: \(x\) and \(y\) are related if and only if

in other words if their difference tends to \(0\).

We have that \(R\) is an equivalence relation. From now on, we will write \(x \approx y\) for \(x R y\).

\(R\) is a reflexive relation.

\(R\) is a symmetric relation.

\(R\) is a transitive relation.

We define the zero of \(\mathrm{MyPrereal}\) as the constant sequence \(0\).

The zero of \(\mathrm{MyPrereal}\) is nonnegative.

We define our rationals \(\mathrm{MyRat}\) as

We will write \(⟦ (a, b) ⟧\) for the class of \((a,b)\).

We define the addition of \(x = ⟦ (a, b) ⟧\) and \(y = ⟦ (c, d) ⟧\) in \(\mathrm{MyRat}\) as

Thanks to Lemma 73 this is well defined.

Let \(x\), \(y\) and \(z\) in \(\mathrm{MyRat}\) be such that \(x \leq y\). Then \(x + z \leq y + z\).

For every \(x\) in \(\mathrm{MyRat}\) there exists \(n\) in \(\mathrm{MyNat}\) such that \(x \leq i(n)\).

\(\mathrm{MyRat}\) with addition and multiplication is a commutative ring.

\(\mathrm{MyRat}\) with addition and multiplication is a field.

We define a map

For all \(a\) and \(b\) in \(\mathrm{MyNat}\) we have that

We have that \(i\) is injective.

Let \(x\) and \(y\) in \(\mathrm{MyNat}\). We have that \(i(x) \leq i(y)\) if and only if \(x \leq y\).

For all \(a\) and \(b\) in \(\mathrm{MyNat}\) we have that

We have that \(i(1) = 1\).

We have that \(i(0) = 0\).

We define the inverse of \(x = ⟦ (a, b) ⟧\) in \(\mathrm{MyRat}\) as

Thanks to Lemma 77 this is well defined.

Given \(x\) in \(\mathrm{MyRat}\), we say that \(x\) is nonnegative if it has a representative with nonnegative numerator and positive denominator: there exist \(a\) and \(b\) in \(\mathrm{MyInt}\) with \(0 \leq a\) and \(0 {\lt} b\) such that

This is the usual condition \(0 \leq a/b\) after choosing a positive denominator.

Let \(x\) and \(y\) be in \(\mathrm{MyRat}\) both nonnegative. Then \(x+y\) is nonnegative.

Let \(x\) be in \(\mathrm{MyRat}\) be nonnegative. Then \(x^{-1}\) is nonnegative.

Let \(x\) and \(y\) be in \(\mathrm{MyRat}\) both nonnegative. Then \(x*y\) is nonnegative.

We define a map

For all \(a\) and \(b\) in \(\mathrm{MyInt}\) we have that

Let \(n\) be a natural number. Then \(\mathrm{MyRat}.j (\mathrm{MyInt}.i (n)) = \mathrm{MyRat}.i (n)\).

We have that \(j\) is injective.

Let \(x\) and \(y\) in \(\mathrm{MyInt}\). We have that \(j(x) \leq j(y)\) if and only if \(x \leq y\).

For all \(a\) and \(b\) in \(\mathrm{MyInt}\) we have that

We have that \(j(1) = 1\).

We have that \(j(0) = 0\).

Let \(x\) and \(y\) in \(\mathrm{MyRat}\). We write \(x \leq y\) if \(y - x\) is nonnegative.

The relation \(\leq \) on \(\mathrm{MyRat}\) is antisymmetric.

The relation \(\leq \) on \(\mathrm{MyRat}\) is reflexive.

The order \(\leq \) on \(\mathrm{MyRat}\) is a total order.

The relation \(\leq \) on \(\mathrm{MyRat}\) is transitive.

We have that \(\mathrm{MyRat}\) with \(\leq \) is a linear order

We define the multiplication of \(x = ⟦ (a, b) ⟧\) and \(y = ⟦ (c, d) ⟧\) in \(\mathrm{MyRat}\) as

Thanks to Lemma 75 this is well defined.

Let \(x \neq 0\) be in \(\mathrm{MyRat}\). Then \(x * x^{-1} = 1\).

Let \(x\) and \(y\) in \(\mathrm{MyRat}\) be such that \(0 \leq x\) and \(0 \leq y\). Then \(0 \leq x * y\).

Let \(x\) and \(y\) in \(\mathrm{MyRat}\) be such that \(0 {\lt} x\) and \(0 {\lt} y\). Then \(0 {\lt} x * y\).

We define the negation of \(x = ⟦ (a, b) ⟧\) in \(\mathrm{MyRat}\) as

Thanks to Lemma 71 this is well defined.

Let \(x\) be in \(\mathrm{MyRat}\) such that both \(x\) and \(-x\) are nonnegative. Then \(x = 0\).

Let \(x\) be in \(\mathrm{MyRat}\) such that \(x\) is not nonnegative. Then \(-x\) is nonnegative.

We define the one of \(\mathrm{MyRat}\), denoted \(1\) as the class of \((1,1)\) (note that \(1 \neq 0\) in \(\mathrm{MyInt}\)).

We have that \(1\) in \(\mathrm{MyRat}\) is nonnegative.

Let \(a\) and \(b\) be in \(\mathrm{MyInt}\) with \(b \neq 0\). Then \(⟦ (a, b) ⟧ = j(a)*j(b)^{-1}\).

We define the zero of \(\mathrm{MyRat}\), denoted \(0\) as the class of \((0,1)\) (note that \(1 \neq 0\) in \(\mathrm{MyInt}\)).

We have that \(0 \leq x\) if and only if \(x\) is nonnegative.

In \(\mathrm{MyRat}\) we have that \(0 \leq 1\).

In \(\mathrm{MyRat}\) we have \(0 \neq 1\).

We have that \(0\) in \(\mathrm{MyRat}\) is nonnegative.

We define our reals \(\mathrm{MyReal}\) as

We will write \(⟦ x ⟧\) for the class of the Cauchy sequence \(x\).

We define the addition of \(⟦ x ⟧\) and \(⟦ y ⟧\) in \(\mathrm{MyReal}\) as \(⟦ x + y ⟧\). Thanks to Lemma 139 this is well defined.

Let \(x\), \(y\) and \(t\) in \(\mathrm{MyReal}\) be such that \(x \leq y\). Then \(x + t \leq y + t\).

Given \(f \colon \mathrm{MyNat}\to \mathrm{MyReal}\), we define \(\mathrm{approx}(f) \colon \mathrm{MyNat}\to \mathrm{MyRat}\) to be a choice of rational approximating sequence as in Lemma 211.

If \(f \colon \mathrm{MyNat}\to \mathrm{MyReal}\) is a Cauchy sequence, then \(\mathrm{approx}(f)\) is a Cauchy sequence of rationals.

For all \(n\) we have \(|f_n - k(\mathrm{approx}(f)_n)| {\lt} k(i(n+1)^{-1})\).

Let \(x\) in \(\mathrm{MyReal}\). Then there exists a natural number \(n\) such that \(x \leq k(i(n+1))\), where \(i \colon \mathrm{MyNat}\to \mathrm{MyRat}\) is the inclusion.

Let \(x\) in \(\mathrm{MyReal}\) with \(0 {\lt} x\). Then there exists a natural number \(n\) such that \(k(i(n+1)^{-1}) \leq x\).

\(\mathrm{MyReal}\) with addition and multiplication is a commutative ring.

\(\mathrm{MyReal}\) is complete: every Cauchy sequence \(f \colon \mathrm{MyNat}\to \mathrm{MyReal}\) is convergent.

Let \(x\) be in \(\mathrm{MyReal}\) such that both \(x\) and \(-x\) are nonnegative. Then \(x = 0\).

Let \(f \colon \mathrm{MyNat}\to \mathrm{MyReal}\). Then there exists \(g \colon \mathrm{MyNat}\to \mathrm{MyRat}\) such that \(|f_n - k(g_n)| {\lt} k(i(n+1)^{-1})\) for all \(n\).

Let \(x\) in \(\mathrm{MyReal}\) and \(n\) a natural number. Then there exists a rational \(r\) such that \(|x - k(r)| {\lt} k(i(n+1)^{-1})\).

\(\mathrm{MyReal}\) with addition and multiplication is a field.

We define the inverse of \(⟦ x ⟧\) in \(\mathrm{MyReal}\) as \(⟦ x^{-1} ⟧\). Thanks to Lemma 145 this is well defined.

A sequence \(f \colon \mathrm{MyNat}\to \mathrm{MyReal}\) is a Cauchy sequence if

If \(f \colon \mathrm{MyNat}\to \mathrm{MyReal}\) is a Cauchy sequence, then \(\mathrm{approx}(f)\), being a Cauchy sequence of rationals, defines an element of \(\mathrm{MyPrereal}\).

A sequence \(f \colon \mathrm{MyNat}\to \mathrm{MyReal}\) is convergent if it tends to some \(x\) in \(\mathrm{MyReal}\).

We say that \(⟦ x ⟧\) in \(\mathrm{MyReal}\) is nonnegative if \(x\) is nonnegative. Thanks to Lemma 179 this does not depend on the representative.

Let \(x\) and \(y\) in \(\mathrm{MyReal}\) both nonnegative. Then \(x + y\) is nonnegative.

Let \(x\) and \(y\) in \(\mathrm{MyReal}\) both nonnegative. Then \(x * y\) is nonnegative.

We define a map

sending a rational to the class of the corresponding constant sequence.

For all \(x\) and \(y\) in \(\mathrm{MyRat}\) we have that \(k(x + y) = k(x) + k(y)\).

We have that \(k\) is injective.

For all \(x\) in \(\mathrm{MyRat}\) we have that \(k(x^{-1}) = k(x)^{-1}\).

Let \(x\) and \(y\) in \(\mathrm{MyRat}\). We have that \(k(x) \leq k(y)\) if and only if \(x \leq y\).

Let \(x\) and \(y\) in \(\mathrm{MyRat}\). We have that \(k(x) {\lt} k(y)\) if and only if \(x {\lt} y\).

For all \(x\) and \(y\) in \(\mathrm{MyRat}\) we have that \(k(x * y) = k(x) * k(y)\).

For all \(x\) in \(\mathrm{MyRat}\) we have that \(k(-x) = -k(x)\).

We have that \(k(1) = 1\).

For all \(x\) and \(y\) in \(\mathrm{MyRat}\) we have that \(k(x - y) = k(x) - k(y)\).

We have that \(k(0) = 0\).

Let \(x\) and \(y\) in \(\mathrm{MyReal}\). We write \(x \leq y\) if \(y - x\) is nonnegative.

The relation \(\leq \) on \(\mathrm{MyReal}\) is antisymmetric.

The relation \(\leq \) on \(\mathrm{MyReal}\) is reflexive.

The order \(\leq \) on \(\mathrm{MyReal}\) is a total order.

The relation \(\leq \) on \(\mathrm{MyReal}\) is transitive.

We have that \(\mathrm{MyReal}\) with \(\leq \) is a linear order.

We define the multiplication of \(⟦ x ⟧\) and \(⟦ y ⟧\) in \(\mathrm{MyReal}\) as \(⟦ x * y ⟧\). Thanks to Lemma 141 this is well defined.

Let \(x \neq 0\) be in \(\mathrm{MyReal}\). Then \(x * x^{-1} = 1\).

Let \(x\) and \(y\) in \(\mathrm{MyReal}\) be such that \(0 \leq x\) and \(0 \leq y\). Then \(0 \leq x * y\).

Let \(a\) and \(b\) in \(\mathrm{MyReal}\) be such that \(0 {\lt} a\) and \(0 {\lt} b\). Then \(0 {\lt} a * b\).

Let \(x\) in \(\mathrm{MyReal}\) with \(0 {\lt} x\). Then there exists \(r\) in \(\mathrm{MyRat}\) with \(0 {\lt} r\) and \(k(r) {\lt} x\).

Let \(x\) in \(\mathrm{MyReal}\) and let \(\varepsilon \) in \(\mathrm{MyReal}\) with \(0 {\lt} \varepsilon \). Then there exists \(r\) in \(\mathrm{MyRat}\) with \(|x - k(r)| {\lt} \varepsilon \).

Let \(x\) in \(\mathrm{MyReal}\) and let \(\varepsilon \) in \(\mathrm{MyRat}\) with \(0 {\lt} \varepsilon \). Then there exists \(r\) in \(\mathrm{MyRat}\) with \(|x - k(r)| {\lt} k(\varepsilon )\).

We define the negation of \(⟦ x ⟧\) in \(\mathrm{MyReal}\) as \(⟦ -x ⟧\). Thanks to Lemma 137 this is well defined.

We define the one of \(\mathrm{MyReal}\), denoted \(1\), as the class of the one of \(\mathrm{MyPrereal}\).

A sequence \(f \colon \mathrm{MyNat}\to \mathrm{MyReal}\) tends to \(x\) in \(\mathrm{MyReal}\) if

Let \(x\) in \(\mathrm{MyPrereal}\). Then the sequence \(n \mapsto k(x_n)\) tends to \(⟦ x ⟧\).

Let \(f \colon \mathrm{MyNat}\to \mathrm{MyReal}\) and \(x\) in \(\mathrm{MyReal}\). If for every rational \(\varepsilon {\gt} 0\) there exists \(N\) such that \(|f_n - x| \leq k(\varepsilon )\) for all \(n \geq N\), then \(f\) tends to \(x\).

We define the zero of \(\mathrm{MyReal}\), denoted \(0\), as the class of the zero of \(\mathrm{MyPrereal}\).

We have that \(0 \leq x\) if and only if \(x\) is nonnegative.

In \(\mathrm{MyReal}\) we have that \(0 \leq 1\).

In \(\mathrm{MyReal}\) we have \(0 \neq 1\).

The zero of \(\mathrm{MyReal}\) is nonnegative.