## Stream: general

### Topic: with_infty

#### Johan Commelin (Oct 08 2018 at 07:01):

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 (Oct 08 2018 at 07:01):

that's with_top

#### Johan Commelin (Oct 08 2018 at 07:02):

I know. But why do we have with_zero?

#### Johan Commelin (Oct 08 2018 at 07:02):

It is just with_bot.

#### Mario Carneiro (Oct 08 2018 at 07:02):

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

#### Mario Carneiro (Oct 08 2018 at 07:02):

with_zero and with_bot are not the same on algebra stuff

I see

#### Johan Commelin (Oct 08 2018 at 07:03):

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

#### Johan Commelin (Oct 08 2018 at 07:03):

Because that might be nice...

#### Mario Carneiro (Oct 08 2018 at 07:05):

yes, ∞ is not a notation associated to any typeclass

#### Mario Carneiro (Oct 08 2018 at 07:05):

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

#### Johan Commelin (Oct 08 2018 at 07:07):

Hmmm, I would vote for keeping the notation.

#### Mario Carneiro (Oct 08 2018 at 07:08):

I think I hit a dependency problem anyway

#### Mario Carneiro (Oct 08 2018 at 07:08):

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

#### Simon Hudon (Oct 08 2018 at 17:13):

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 (Oct 10 2018 at 17:24):

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

#### Johannes Hölzl (Oct 10 2018 at 17:25):

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.

Last updated: May 14 2021 at 22:15 UTC