The extended reals [-∞, ∞]. #
Addition and multiplication are problematic in the presence of ±∞, but negation has a natural definition and satisfies the usual properties.
An ad hoc addition is defined, for which
ereal is an
add_comm_monoid, and even an ordered one
a ≤ a' and
b ≤ b' then
a + b ≤ a' + b').
Note however that addition is badly behaved at
(⊥, ⊤) and
(⊤, ⊥) so this can not be upgraded
to a group structure. Our choice is that
⊥ + ⊤ = ⊤ + ⊥ = ⊤.
An ad hoc subtraction is then defined by
x - y = x + (-y). It does not have nice properties,
but it is sometimes convenient to have.
ℝ and from
ℝ≥0∞ are registered, and their basic properties are proved. The main
one is the real coercion, and is usually referred to just as
coe (lemmas such as
ereal.coe_add deal with this coercion). The one from
ennreal is usually called
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
A recursor for
ereal in terms of the coercion.
When working in term mode, note that pattern matching can be used directly.
Real coercion #
ennreal coercion #
The set of numbers in
ereal that are not equal to
±∞ is equivalent to
ereal, defined by
x - y = x + (-y). Since addition is badly behaved at some
points, so is subtraction. There is no standard algebraic typeclass involving subtraction that is
ereal because of this bad behavior.