The reals in mathlib

Mathematical background

[this should also be in the other ch3 about fake reals]

According to Wikipedia, real numbers form the unique Dedekind-complete ordered field (R ; + ; · ; <), up to an isomorphism,[a]

The real numbers \(\mathbb{R}\) are a complete totally-ordered field, and also a metric space.

Some fundamental theorems about the real numbers:

  1. We have 0 < 1.

  2. The topology defined by the metric is equal to the topology defined by the order.

    1. The Intermediate Value Theorem.

    2. The Mean Value Theorem.

    3. The reals are the unique complete totally-ordered field.

      Not all of these are in Lean.

In the last chapter we saw how to build such a structure using axioms. The topologies