kdrag.theories.real.seq

Module Attributes

cauchy_mod

is_convergent = kd.define(

Functions

test()

Classes

Series()

class kdrag.theories.real.seq.Series

Bases: object

powers = powers

kdrag.theories.real.seq.cauchy_mod = cauchy_mod

is_convergent = kd.define(

“is_convergent”, [a], kd.QForAll(

[eps], eps > 0, smt.Exists(

[N], kd.QForAll([m], m > N, smt.Exists([x], real.abs(a[m] - x) < eps))

),

),

)

kdrag.theories.real.seq.test()

>>> True
True