English
FundamentalSequenceProp o is the property characterizing the fundamental sequence: it specifies the behavior for zero, successor, and limit cases, capturing how o is decomposed into simpler pieces.
Русский
FundamentalSequenceProp o — свойство, описывающее фундаментальную последовательность: задаёт поведение нулевого, последовательного и предельного случаев, фиксируя разложение o на более простые части.
LaTeX
$$$\\text{FundamentalSequenceProp}(o) : (Option\\ ONote) \\oplus (\\mathbb{N} \\rightarrow ONote) \\rightarrow Prop$ with the cases as defined in the theorem$$
Lean4
/-- The property satisfied by `fundamentalSequence o`:
* `inl none` means `o = 0`
* `inl (some a)` means `o = succ a`
* `inr f` means `o` is a limit ordinal and `f` is a strictly increasing sequence which converges to
`o` -/
def FundamentalSequenceProp (o : ONote) : (Option ONote) ⊕ (ℕ → ONote) → Prop
| Sum.inl none => o = 0
| Sum.inl (some a) => o.repr = succ a.repr ∧ (o.NF → a.NF)
| Sum.inr f =>
IsSuccLimit o.repr ∧ (∀ i, f i < f (i + 1) ∧ f i < o ∧ (o.NF → (f i).NF)) ∧ ∀ a, a < o.repr → ∃ i, a < (f i).repr
