English
FundamentalSequenceProp applied to Sum.inr f describes limit ordinal behavior: IsSuccLimit o.repr and the sequence f increases and stays below o, with a convergence property to o.
Русский
FundamentalSequenceProp для Sum.inr f описывает поведение при предельном ординале: IsSuccLimit o.repr и последовательность f возрастает и ограничена снизу o, с свойством предельного перехода к o.
LaTeX
$$$\\text{FundamentalSequenceProp}(o)(\\text{Sum.inr } f) \\iff IsSuccLimit(o.repr) \\land (\\forall i, f(i) < f(i+1) \\land f(i) < o \\land (o.NF \\rightarrow (f(i)).NF)) \\land \\forall a, a < o.repr \\rightarrow \\exists i, a < (f(i)).repr$$$
Lean4
theorem fundamentalSequenceProp_inr (o f) :
FundamentalSequenceProp o (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 :=
Iff.rfl
