The extended reals [-∞, ∞].
This file defines ereal, the real numbers together with a top and bottom element,
referred to as ⊤ and ⊥. It is implemented as with_top (with_bot ℝ)
Addition and multiplication are problematic in the presence of ±∞, but
negation has a natural definition and satisfies the usual properties.
An addition is derived, but ereal is not even a monoid (there is no identity).
ereal is a complete_lattice; this is now deduced by type class inference from
the fact that with_top (with_bot L) is a complete lattice if L is
a conditionally complete lattice.
Tags
real, ereal, complete lattice
TODO
abs : ereal → ennreal
In Isabelle they define + - * and / (making junk choices for things like -∞ + ∞) and then prove whatever bits of the ordered ring/field axioms still hold. They also do some limits stuff (liminf/limsup etc). See https://isabelle.in.tum.de/dist/library/HOL/HOL-Library/Extended_Real.html