Membership syntax for anonymous function

Stream: new members

[Jakub Nowak]

I'm trying to take lsub of ordinals over a list. I could use docs#iSub because it has syntax for docs#Membership. Is there a syntax for docs#Membership for anonymous functions so I can use it with docs#Ordinal.lsub?

import Mathlib

variable (os : List Ordinal.{0})

#check 1 + ⨆ o ∈ os, o

#check ((Ordinal.lsub (fun (o : { o | o ∈ os }) ↦ o.val)) : Ordinal.{0})

The second #check doesn't work, and I don't understand why.

[Robin Arnez]

It's a universe problem, lsub has the weird type of def lsub {ι : Type u} (f : ι → Ordinal.{max u v}) : Ordinal.{max u v} (for some reason...). There are also comments in the code suggesting that lsub should be deprecated; I guess you're supposed to use ⨆ o ∈ os, Order.succ o instead?

[Violeta Hernández]

You should not be using docs#Ordinal.lsub.

[Violeta Hernández]

I haven't been able to deprecate it, but you should treat it as morally deprecated

[Aaron Liu]

yeah weren't we gonna remove it

[Violeta Hernández]

To do what you want you could do (os.map (fun x ↦ x + 1)).max

[Violeta Hernández]

To take the least strict upper bound of a set s, use sSup ((fun x ↦ x + 1) '' s)

[Violeta Hernández]

lsub inevitably leads to universe issues like the one you just came across

[Mirek Olšák]

Oh, sorry, my bad

[Mirek Olšák]

It seemed universe-wise reasonable to me for the purpose in #new members > Showing termination with high-order inductive @ 💬

[Mirek Olšák]

I thought this universe constraint makes a lot of sense -- exactly because of the smaller universe, you know there is an ordinal above. If you took arbitrary set of ordinals, such as the set of all the ordinals, you would not have this guarantee.

[Violeta Hernández]

The actual constraint you'd want is not a universe constraint, but rather a constraint that your set be docs#Small

[Violeta Hernández]

For instance, one can always take the supremum of the range of a function Iio x → Ordinal.{u} for some x : Ordinal.{u}, even though the domain is in Type (u + 1)

[Mirek Olšák]

I think in Jakub's case, writing

#check (Ordinal.lsub (fun i : Fin os.length ↦ os[i]) : Ordinal.{0})

would be reasonable. But if you want to deprecate it...

[Violeta Hernández]

Yes, lsub was added by me back in 2021 or so, before the Ordinal API was even linked to the much more expansive API on conditionally complete orders.

[Violeta Hernández]

For that and other reasons I'd suggest just using sSup / iSup

[Mirek Olšák]

But supremum is a little different operation from smallest strict upper bound. Isn't the latter often more practical for ordinals?

[Mirek Olšák]

Even if you change it to an operation on Set Ordinal which are Small...

[Violeta Hernández]

Well, to be more precise, my suggestion is using sSup / iSup composed with (· + 1)

[Violeta Hernández]

We could in theory redefine lsub for a conditionally complete lattice with a successor function, but that seems like unnecessary cruft

[Mirek Olšák]

It makes the proofs in my example of a well-founded recursion a little more complicated but what can I do...

[Mirek Olšák]

Mirek Olšák said:

It seemed universe-wise reasonable to me for the purpose in #new members > Showing termination with high-order inductive @ 💬

I updated the code here, so check if it contains some any other deprecated recommendations...

[Mirek Olšák]

On the other hand, @Jakub Nowak , I think you should be realizing what you are doing. I am not sure how much set theory you know, so sorry if I am saying trivialities.

Most mathematicians consider mathematics is done in ZFC -- that is an axiomatic framework (a little different from Lean but comparable). The world of ZFC is rich enough for almost all of mathematics in the world.

Defining an inductive datatype of type Type 1, is quite extraordinary, and on par with how Lean defines the entire ZFC universe (docs#PSet). When you have an inductive

inductive ListSchema : Type → Type 1 where
| nil : ListSchema α
| cons (x : α) (xs : ListSchema α) : ListSchema α
| fmap (xs : ListSchema α) (f : α → ListSchema β) : ListSchema β

it means that in fmap, you "store" a node for each element "x : α" , where "α" can be arbitrarily large, infinite, uncountable, or way way bigger ...

And it is not only the width that can explode. Although every single branch in the tree will be finite, there is no bound on how "high" a node can be either. If you have an infinitely branching tree with branches of lengths 0, 1, 2, ..., you have to give the main node the level ω, if you put such node into a tree, that tree will have height ω+1, ω+2, etc. But there are much more ordinals, some ordinals are uncountable. Actually for arbitrary large set / type, there is an ordinal which has as many nodes below itself. So ordinals are again spanning the entire ZFC universe (they have the same cardinality as all the ZFC-sets)...

So in standard mathematics, you would be already hitting its limits. In particular, if you consider all the heights of all the ListSchema, you will fill all the standard ordinals, there is no Ordinal.{0} which would be above all such heights. Are you sure it is what you intend?

Lean can do a little more, it has infinitely many such universes above each other (called Type 0, Type 1, Type 2 ...), similarly it has also Ordinal.{1}, Ordinal.{2} and that is the limit of Lean. You cannot build the sigma type Σ n : ℕ, Type n, you cannot even take Type (10^100). Because universes are the limit of Lean, it can get a bit confusing if you don't know precisely how you are using them.