GeneralizedContinuedFraction.terminated_stable
theorem GeneralizedContinuedFraction.terminated_stable :
∀ {K : Type u_1} {g : GeneralizedContinuedFraction K} {n m : ℕ}, n ≤ m → g.TerminatedAt n → g.TerminatedAt m := by
sorry
This theorem states that for any type `K`, any generalized continued fraction `g` of type `K`, and any natural numbers `n` and `m`, if the generalized continued fraction `g` terminated at position `n` and `m` is greater than or equal to `n`, then `g` also terminated at position `m`. In other words, the termination of a generalized continued fraction at a certain position ensures its termination at all positions greater or equal to it.
More concisely: If a generalized continued fraction of type `K` terminates at position `n`, then it also terminates at position `m` for any `m >= n`.
|