with_infty

Stream: general

[Johan Commelin]

I am looking at Sebastien's PR for emetric spaces. And I'm wondering, we have with_top, with_bot and with_zero. Would it make sense to have with_infty, or is it not worth it?

[Mario Carneiro]

that's with_top

[Johan Commelin]

I know. But why do we have with_zero?

[Johan Commelin]

It is just with_bot.

[Mario Carneiro]

I think there are some algebraic definitions on with_top, and they correspond to treating it like infinity

[Mario Carneiro]

with_zero and with_bot are not the same on algebra stuff

[Johan Commelin]

I see

[Johan Commelin]

So if someone wants to use ∞ notation, they should just introduce it locally?

[Johan Commelin]

Because that might be nice...

[Mario Carneiro]

yes, ∞ is not a notation associated to any typeclass

[Mario Carneiro]

indeed I was thinking of eliminating it from ennreal in favor of top everywhere

[Johan Commelin]

Hmmm, I would vote for keeping the notation.

[Mario Carneiro]

I think I hit a dependency problem anyway

[Mario Carneiro]

but it's a local notation, use what you like

[Simon Hudon]

Do you ever add both a bottom and a top? In what order do you add them? Or do you build it as a sum bool a?

[Johannes Hölzl]

fyi: ∞ is only a local notation for top. https://github.com/leanprover/mathlib/blob/master/data/real/ennreal.lean#L19

[Johannes Hölzl]

I don't think we currently have a case where we add a top and a bot. But we add top to structures which already have a bot, like ennreal, or enat.