Zulip Chat Archive

Stream: maths

Topic: Sups of ℕ and infinity


view this post on Zulip Eric Rodriguez (Apr 08 2021 at 12:30):

Is there any natural way to write noncomputable def my_def := Sup {n : ℕ | P n} such that my_def is in ℕ ∪ {∞} (or I guess in Lean, enat? I couldn't find anything, apart from maybe using with_top with_bot ℕ, but that seems unwise. It'd be really nice for me to say that if P n, then n ≤ my_def.

view this post on Zulip Kevin Buzzard (Apr 08 2021 at 12:32):

Apparently enat is not a complete lattice (unless I'm missing an import) (or it's not true).

view this post on Zulip Eric Rodriguez (Apr 08 2021 at 12:33):

Should Sup ø be zero or bot? Hmm

view this post on Zulip Kevin Buzzard (Apr 08 2021 at 12:34):

indeed neither enat nor with_top ℕ appear to be instances of the has_Sup typeclass.

view this post on Zulip Kevin Buzzard (Apr 08 2021 at 12:34):

wait -- are you adding a bot or not?

view this post on Zulip Eric Rodriguez (Apr 08 2021 at 12:34):

No, was just speculating as to why enat couldn't be a complete lattice

view this post on Zulip Kevin Buzzard (Apr 08 2021 at 12:34):

The sup of the empty set is 0 in enat -- it satisfies all the axioms.

view this post on Zulip Kevin Buzzard (Apr 08 2021 at 12:35):

It might be a fun exercise to try and put a complete lattice structure on enat (once someone has independently verified that it's not there already).

view this post on Zulip Eric Rodriguez (Apr 08 2021 at 12:36):

Alright, in that case I'll get cracking on it!

view this post on Zulip Kevin Buzzard (Apr 08 2021 at 12:37):

you might find that something doesn't work, and then that will be the reason it's not there :-)

view this post on Zulip Kevin Buzzard (Apr 08 2021 at 12:37):

But order-theoretically it looks isomorphic to a closed and bounded subset of the reals so I think it should work...

view this post on Zulip Kevin Buzzard (Apr 08 2021 at 12:38):

I guess there might also be some trick involving complete lattice structures on successor ordinals -- is that a thing?

view this post on Zulip Eric Wieser (Apr 08 2021 at 12:47):

with_top \N works for that case I think

view this post on Zulip Ruben Van de Velde (Apr 08 2021 at 12:47):

with_top and nat are listed at https://leanprover-community.github.io/mathlib_docs/order/complete_lattice.html#has_Sup.Sup , at least

view this post on Zulip Eric Wieser (Apr 08 2021 at 12:50):

You might need to import order.conditionally_complete_lattice

view this post on Zulip Yury G. Kudryashov (Apr 08 2021 at 15:18):

See docs#enat.complete_linear_order

view this post on Zulip Yury G. Kudryashov (Apr 08 2021 at 15:19):

If you have p : nat → Prop, then you can use ⨆ (n : nat) (hn : P n), (n : enat), see docs#formal_multilinear_series.radius for an example with nnreal and ennreal.


Last updated: May 06 2021 at 18:20 UTC