Sups of ℕ and infinity

Stream: maths

[Eric Rodriguez]

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.

[Kevin Buzzard]

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

[Eric Rodriguez]

Should Sup ø be zero or bot? Hmm

[Kevin Buzzard]

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

[Kevin Buzzard]

wait -- are you adding a bot or not?

[Eric Rodriguez]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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).

[Eric Rodriguez]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Eric Wieser]

with_top \N works for that case I think

[Ruben Van de Velde]

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

[Eric Wieser]

You might need to import order.conditionally_complete_lattice

[Yury G. Kudryashov]

See docs#enat.complete_linear_order

[Yury G. Kudryashov]

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.