feat(SetTheory/Ordinal/Basic): notation `typeLT α = type (α := α) (· < ·)`

[vihdzp]

---

Another option might be to simply make the type argument in type explicit, but since the API makes a lot of use of unbundled relations, that would just make a lot of code longer.

This might also make sense to have for typein, but currently we use typein (α := o.toType) (· < ·) a lot when we should be using Ordinal.enumIsoToType instead, so I'd like to clean that up before seeing if introducing notation makes sense.