Zulip Chat Archive
Stream: maths
Topic: supremum is real or infinite
Apurva Nakade (Jul 04 2023 at 02:19):
How best to encode that supremum of a set of real numbers is either real number or infinite? Is there a variant of ENNReal but for all real numbers?
Mario Carneiro (Jul 04 2023 at 02:20):
Mario Carneiro (Jul 04 2023 at 02:20):
you could also use WithTop Real
Mario Carneiro (Jul 04 2023 at 02:21):
although I guess if you allow the empty set then both infinities are possible
Apurva Nakade (Jul 04 2023 at 02:25):
Thanks! I'll read this file in more details.
So is there a sSup whose target is EReal? I'm a bit confused by how the default target of sSup is Real.
Apurva Nakade (Jul 04 2023 at 02:26):
(I guess I can coerce my set to be valued in EReals...)
Mario Carneiro (Jul 04 2023 at 02:27):
sSup is only well defined when the set has a supremum
Apurva Nakade (Jul 04 2023 at 02:28):
Ahh, thanks!
Yury G. Kudryashov (Jul 04 2023 at 02:42):
We have docs#isLUB_csSup
Apurva Nakade (Jul 04 2023 at 06:27):
I see, so the concepts of LUB and Sup are defined independently. I hadn't thought about this distinction before. I'll need to see which one of the two I want. Thanks!
Last updated: Dec 20 2023 at 11:08 UTC