The extended reals [-∞, ∞]. #
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).
real, ereal, complete lattice
abs : ereal → ℝ≥0∞
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