rw with `mk_initialSeg`

Stream: mathlib4

[Nir Paz]

What do you think of changing Ordinal.mk_initialSeg to be written with Iio o rather than { o' : Ordinal | o' < o }? Or even adding a version with it. Currently I do something like change ... #{p | _} ... every time I rw with it.

@Violeta Hernández

[Nir Paz]

Just changing it doesn't break anything

[Violeta Hernández]

I think that's unambiguously good. It should also be called mk_Iio_ordinal

[Ruben Van de Velde]

If you find yourself using change, you almost certainly need to add a lemma, yeah

[Nir Paz]

#16929

[Nir Paz]

Apparantly mk_initialSeg is only used once in mathlib

[Violeta Hernández]

I actually wanted to use this exact lemma yesterday! I just forgot it had that weird name.

[Nir Paz]

It's funny, I feel like I use it all the time

[Nir Paz]

In a similar vein: aleph_isNormal : IsNormal (ord ∘ aleph) is annoying to work with (for example everything we have on iSup uses the ⨆ notation). We can change it to IsNormal (fun o ↦ (aleph o).ord).

[Violeta Hernández]

I feel like this might be an XY. It'd be nice not to have to work with ord ⚬ aleph at all and simply have a function omega for this.

[Violeta Hernández]

Just, named differently

[Violeta Hernández]

I just opened #16964. I did it to golf the definition of aleph later down the line, but it could also be used to define this omega function first. It'd be the enumerator function of initial ordinals.

[Violeta Hernández]

I half-recall proposing this at some point, but I imagine my proposed rename omega → omega₀ didn't make people too happy. Might be misremembering though.

[Nir Paz]

To be honest it doesn't make me happy either, but having an omega function is worth it.

[Nir Paz]

Actually as long as the notation for it works it doesn't really matter anyways