Zulip Chat Archive

Stream: general

Topic: with_infty


view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Oct 08 2018 at 07:01):

that's with_top

view this post on Zulip Johan Commelin (Oct 08 2018 at 07:02):

I know. But why do we have with_zero?

view this post on Zulip Johan Commelin (Oct 08 2018 at 07:02):

It is just with_bot.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Oct 08 2018 at 07:02):

with_zero and with_bot are not the same on algebra stuff

view this post on Zulip Johan Commelin (Oct 08 2018 at 07:03):

I see

view this post on Zulip Johan Commelin (Oct 08 2018 at 07:03):

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

view this post on Zulip Johan Commelin (Oct 08 2018 at 07:03):

Because that might be nice...

view this post on Zulip Mario Carneiro (Oct 08 2018 at 07:05):

yes, is not a notation associated to any typeclass

view this post on Zulip Mario Carneiro (Oct 08 2018 at 07:05):

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

view this post on Zulip Johan Commelin (Oct 08 2018 at 07:07):

Hmmm, I would vote for keeping the notation.

view this post on Zulip Mario Carneiro (Oct 08 2018 at 07:08):

I think I hit a dependency problem anyway

view this post on Zulip Mario Carneiro (Oct 08 2018 at 07:08):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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