Does mathlib have infinity and a type of extended reals?

Stream: Is there code for X?

[Lars Ericson]

In mathlib I see "native float infinity". I don't immediately see the "conceptual" infinity. Two questions:

Q1. Where is abstract infinity oo in mathlib?
Q2. Is there a definition of "extended reals" that is something like Rbar = R + {-oo, oo}?

[Yakov Pechersky]

docs#ereal

[Yury G. Kudryashov]

We have docs#real, docs#nnreal, docs#ennreal, and docs#ereal

[Rémy Degenne]

note that ereal is rather incomplete : it looks like it does not have has_mul for example. ereal is defined as with_bot(with_top(R)) and the with_top construction comes with a mul, but it looks like the with_bot does not (unless I am missing an order_dual statement somewhere). And even if you wrote a has_mul for with_bot, the resulting mul would be strange : you would have (-1)*(+oo) = +oo (and not -oo like you would maybe expect).

[Damiano Testa]

Also, what would -∞ * +∞ equal?

[Ruben Van de Velde]

37

[Damiano Testa]

You are completely right!!

[Rémy Degenne]

from the order of the with_bot(with_top(R)) construction, assuming that you define the mul of bot as done with top, it would be -oo

[Eric Wieser]

I assume you meant to ask what -∞ + +∞ is? Coming from floating point, -∞ * +∞ = -∞ seems like the obvious choice.

[Damiano Testa]

I thought that it was the multiplication that people were talking about, but you are right, addition also has its problems. However, I now realize that the problems might simply be in my head, since it may in practice not matter much how you define the non-sensical operations. I still need to interiorize the division-by-zero conundrum...

[Rémy Degenne]

I just tested the additive version : for ereal, bot + top = top

[Rémy Degenne]

because I was wrong about the definition : it is ereal = with_top (with_bot ℝ)

[Rémy Degenne]

hence the rule is that for all x in with_bot ℝ, x + top = top

[Kevin Buzzard]

I wrote ereal and because I'm a mathematician and I did not have good answers for things like -infty+infty and 0 * infty I simply did not define them. In the analogous Isabelle code (written by a computer scientist) they're all defined and take on some random values for these weird cases. I'm sure the maintainers would happily accept a PR which adds all these functions and then proves all the lemmas in the Isabelle file (which I think I left a link to in the docstring?). The proofs are all easy by cases of course.