English
The fundamentalSequence o assigns to an ordinal notation either 0 (for 0), a successor notation (for a successor ordinal), or a limit-sequence for a limit ordinal, describing how to approach o via a converging sequence of smaller notations.
Русский
FundamentalSequence o сопоставляет для нотации ординала либо 0 (для 0), либо обозначение продолжения (для последовательного целочисленного предела), либо последовательность пределов для предельного ординала, описывая приближение к o через сходящуюся последовательность меньших нотаций.
LaTeX
$$$\\text{fundamentalSequence} :\\ ONote \\rightarrow (Option\\ ONote) \\oplus (\\mathbb{N} \\rightarrow ONote)$$$
Lean4
/-- Given an ordinal, returns:
* `inl none` for `0`
* `inl (some a)` for `a + 1`
* `inr f` for a limit ordinal `a`, where `f i` is a sequence converging to `a` -/
def fundamentalSequence : ONote → (Option ONote) ⊕ (ℕ → ONote)
| zero => Sum.inl none
| oadd a m b =>
match fundamentalSequence b with
| Sum.inr f => Sum.inr fun i => oadd a m (f i)
| Sum.inl (some b') => Sum.inl (some (oadd a m b'))
| Sum.inl none =>
match fundamentalSequence a, m.natPred with
| Sum.inl none, 0 => Sum.inl (some zero)
| Sum.inl none, m + 1 => Sum.inl (some (oadd zero m.succPNat zero))
| Sum.inl (some a'), 0 => Sum.inr fun i => oadd a' i.succPNat zero
| Sum.inl (some a'), m + 1 => Sum.inr fun i => oadd a m.succPNat (oadd a' i.succPNat zero)
| Sum.inr f, 0 => Sum.inr fun i => oadd (f i) 1 zero
| Sum.inr f, m + 1 => Sum.inr fun i => oadd a m.succPNat (oadd (f i) 1 zero)
